wp.h File Reference

Weakest Preconditions. More...

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Functions
exprt	wp (const codet &code, const exprt &post, const namespacet &ns)
	Compute the weakest precondition of the given program piece code with respect to the expression post.
void	approximate_nondet (exprt &dest)
	Approximate the non-deterministic choice in a way cheaper than by (proper) quantification.

Detailed Description

Weakest Preconditions.

Definition in file wp.h.

Function Documentation

approximate_nondet()

void approximate_nondet

(

exprt &

dest

)

Approximate the non-deterministic choice in a way cheaper than by (proper) quantification.

Definition at line 57 of file wp.cpp.

wp()

exprt wp	(	const codet &	code,
		const exprt &	post,
		const namespacet &	ns
	)

Compute the weakest precondition of the given program piece code with respect to the expression post.

Parameters

code	Program
post	Postcondition
ns	Namespace

Returns

Weakest precondition

Definition at line 239 of file wp.cpp.