cprover
|
Public Member Functions | |
preconditiont (const namespacet &_ns, value_setst &_value_sets, const goto_programt::const_targett _target, const symex_target_equationt::SSA_stept &_SSA_step, const goto_symex_statet &_s) | |
void | compute (exprt &dest) |
Protected Member Functions | |
void | compute_rec (exprt &dest) |
void | compute_address_of (exprt &dest) |
Protected Attributes | |
const namespacet & | ns |
value_setst & | value_sets |
const goto_programt::const_targett | target |
const symex_target_equationt::SSA_stept & | SSA_step |
const goto_symex_statet & | s |
Definition at line 20 of file precondition.cpp.
|
inline |
Definition at line 23 of file precondition.cpp.
void preconditiont::compute | ( | exprt & | dest | ) |
Definition at line 96 of file precondition.cpp.
References compute_rec().
Referenced by compute_address_of(), and precondition().
|
protected |
Definition at line 72 of file precondition.cpp.
References compute(), irept::id(), exprt::op0(), exprt::op1(), and exprt::operands().
Referenced by compute_rec().
|
protected |
Definition at line 101 of file precondition.cpp.
References compute_address_of(), dereference(), find_symbols(), Forall_operands, ssa_exprt::get_object_name(), ssa_exprt::get_original_expr(), goto_symex_statet::get_original_name(), value_setst::get_values(), irept::id(), ns, exprt::op0(), exprt::operands(), s, symex_target_equationt::SSA_stept::ssa_lhs, symex_target_equationt::SSA_stept::ssa_rhs, SSA_step, irept::swap(), target, and value_sets.
Referenced by compute().
|
protected |
Definition at line 38 of file precondition.cpp.
Referenced by compute_rec().
|
protected |
Definition at line 42 of file precondition.cpp.
Referenced by compute_rec().
|
protected |
Definition at line 41 of file precondition.cpp.
Referenced by compute_rec().
|
protected |
Definition at line 40 of file precondition.cpp.
Referenced by compute_rec().
|
protected |
Definition at line 39 of file precondition.cpp.
Referenced by compute_rec().