cprover
|
Weakest Preconditions. More...
Go to the source code of this file.
Enumerations | |
enum | aliasingt { aliasingt::A_MAY, aliasingt::A_MUST, aliasingt::A_MUSTNOT } |
consider possible aliasing More... | |
Functions | |
bool | has_nondet (const exprt &dest) |
void | approximate_nondet_rec (exprt &dest, unsigned &count) |
void | approximate_nondet (exprt &dest) |
approximate the non-deterministic choice in a way cheaper than by (proper) quantification More... | |
aliasingt | aliasing (const exprt &e1, const exprt &e2, const namespacet &ns) |
void | substitute_rec (exprt &dest, const exprt &what, const exprt &by, const namespacet &ns) |
replace 'what' by 'by' in 'dest', considering possible aliasing More... | |
void | rewrite_assignment (exprt &lhs, exprt &rhs) |
exprt | wp_assign (const code_assignt &code, const exprt &post, const namespacet &ns) |
exprt | wp_assume (const code_assumet &code, const exprt &post, const namespacet &ns) |
exprt | wp_decl (const code_declt &code, const exprt &post, const namespacet &ns) |
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... | |
Weakest Preconditions.
Definition in file wp.cpp.
|
strong |
aliasingt aliasing | ( | const exprt & | e1, |
const exprt & | e2, | ||
const namespacet & | ns | ||
) |
Definition at line 62 of file wp.cpp.
References A_MAY, A_MUST, A_MUSTNOT, base_type_eq(), symbol_exprt::get_identifier(), irept::id(), exprt::op0(), exprt::operands(), to_symbol_expr(), and exprt::type().
Referenced by substitute_rec().
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().
void approximate_nondet_rec | ( | exprt & | dest, |
unsigned & | count | ||
) |
Definition at line 38 of file wp.cpp.
References Forall_operands, side_effect_exprt::get_statement(), irept::id(), irept::set(), and to_side_effect_expr().
Referenced by approximate_nondet().
bool has_nondet | ( | const exprt & | dest | ) |
Definition at line 20 of file wp.cpp.
References forall_operands, side_effect_exprt::get_statement(), irept::id(), and to_side_effect_expr().
Definition at line 164 of file wp.cpp.
References index_exprt::array(), member_exprt::get_component_name(), irept::id(), index_exprt::index(), with_exprt::new_value(), with_exprt::old(), irept::set(), member_exprt::struct_op(), to_index_expr(), to_member_expr(), exprt::type(), and with_exprt::where().
Referenced by wp_assign().
void substitute_rec | ( | exprt & | dest, |
const exprt & | what, | ||
const exprt & | by, | ||
const namespacet & | ns | ||
) |
replace 'what' by 'by' in 'dest', considering possible aliasing
Definition at line 115 of file wp.cpp.
References A_MAY, A_MUST, A_MUSTNOT, aliasing(), if_exprt::cond(), if_exprt::false_case(), Forall_operands, irept::id(), if_exprt::true_case(), and exprt::type().
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().
exprt wp_assign | ( | const code_assignt & | code, |
const exprt & | post, | ||
const namespacet & | ns | ||
) |
Definition at line 202 of file wp.cpp.
References approximate_nondet(), code_assignt::lhs(), rewrite_assignment(), code_assignt::rhs(), and substitute_rec().
exprt wp_assume | ( | const code_assumet & | code, |
const exprt & | post, | ||
const namespacet & | ns | ||
) |
exprt wp_decl | ( | const code_declt & | code, |
const exprt & | post, | ||
const namespacet & | ns | ||
) |
Definition at line 231 of file wp.cpp.
References code_declt::symbol(), exprt::type(), and wp_assign().
Referenced by wp().