cprover
|
Public Member Functions | |
postconditiont (const namespacet &_ns, const value_sett &_value_set, const symex_target_equationt::SSA_stept &_SSA_step, const goto_symex_statet &_s) | |
void | compute (exprt &dest) |
Protected Member Functions | |
void | strengthen (exprt &dest) |
void | weaken (exprt &dest) |
bool | is_used_address_of (const exprt &expr, const irep_idt &identifier) |
bool | is_used (const exprt &expr, const irep_idt &identifier) |
Protected Attributes | |
const namespacet & | ns |
const value_sett & | value_set |
const symex_target_equationt::SSA_stept & | SSA_step |
const goto_symex_statet & | s |
Definition at line 19 of file postcondition.cpp.
|
inline |
Definition at line 22 of file postcondition.cpp.
void postconditiont::compute | ( | exprt & | dest | ) |
Definition at line 99 of file postcondition.cpp.
References strengthen(), and weaken().
Definition at line 151 of file postcondition.cpp.
References find_symbols(), forall_operands, irept::get_bool(), symbol_exprt::get_identifier(), ssa_exprt::get_object_name(), goto_symex_statet::get_original_name(), value_sett::get_value_set(), irept::id(), is_used_address_of(), ns, exprt::op0(), exprt::operands(), s, to_ssa_expr(), to_symbol_expr(), and value_set.
Referenced by is_used_address_of(), strengthen(), and weaken().
|
protected |
Definition at line 69 of file postcondition.cpp.
References irept::id(), is_used(), exprt::op0(), exprt::op1(), and exprt::operands().
Referenced by is_used().
|
protected |
Definition at line 130 of file postcondition.cpp.
References ssa_exprt::get_object_name(), goto_symex_statet::get_original_name(), irept::id(), exprt::is_true(), is_used(), s, symex_target_equationt::SSA_stept::ssa_lhs, symex_target_equationt::SSA_stept::ssa_rhs, SSA_step, irept::swap(), and exprt::type().
Referenced by compute().
|
protected |
Definition at line 108 of file postcondition.cpp.
References Forall_operands, ssa_exprt::get_object_name(), irept::id(), is_used(), symex_target_equationt::SSA_stept::ssa_lhs, SSA_step, and exprt::type().
Referenced by compute().
|
protected |
Definition at line 35 of file postcondition.cpp.
Referenced by is_used().
|
protected |
Definition at line 38 of file postcondition.cpp.
Referenced by is_used(), and strengthen().
|
protected |
Definition at line 37 of file postcondition.cpp.
Referenced by strengthen(), and weaken().
|
protected |
Definition at line 36 of file postcondition.cpp.
Referenced by is_used().