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 94 of file postcondition.cpp.
Definition at line 146 of file postcondition.cpp.
|
protected |
Definition at line 69 of file postcondition.cpp.
|
protected |
Definition at line 125 of file postcondition.cpp.
|
protected |
Definition at line 103 of file postcondition.cpp.
|
protected |
Definition at line 35 of file postcondition.cpp.
|
protected |
Definition at line 38 of file postcondition.cpp.
|
protected |
Definition at line 37 of file postcondition.cpp.
|
protected |
Definition at line 36 of file postcondition.cpp.