cprover
|
Weakest Preconditions. More...
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. More... | |
void | approximate_nondet (exprt &dest) |
approximate the non-deterministic choice in a way cheaper than by (proper) quantification More... | |
Weakest Preconditions.
Definition in file wp.h.
void approximate_nondet | ( | exprt & | dest | ) |
approximate the non-deterministic choice in a way cheaper than by (proper) quantification
Definition at line 53 of file wp.cpp.
References approximate_nondet_rec().
Referenced by wp_assign().
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.
code | Program |
post | Postcondition |
ns | Namespace |
Definition at line 244 of file wp.cpp.
References codet::get_statement(), id2string(), to_code_assign(), to_code_assume(), to_code_decl(), wp_assign(), wp_assume(), and wp_decl().