cprover
|
Public Member Functions | |
preconditiont (const namespacet &_ns, value_setst &_value_sets, const goto_programt::const_targett _target, const 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 SSA_stept & | SSA_step |
const goto_symex_statet & | s |
Definition at line 21 of file precondition.cpp.
|
inline |
Definition at line 24 of file precondition.cpp.
void preconditiont::compute | ( | exprt & | dest | ) |
Definition at line 95 of file precondition.cpp.
|
protected |
Definition at line 73 of file precondition.cpp.
|
protected |
Definition at line 100 of file precondition.cpp.
|
protected |
Definition at line 39 of file precondition.cpp.
|
protected |
Definition at line 43 of file precondition.cpp.
|
protected |
Definition at line 42 of file precondition.cpp.
|
protected |
Definition at line 41 of file precondition.cpp.
|
protected |
Definition at line 40 of file precondition.cpp.