CBMC
Public Member Functions | Protected Member Functions | Protected Attributes | List of all members
postconditiont Class Reference
+ Collaboration diagram for postconditiont:

Public Member Functions

 postconditiont (const namespacet &_ns, const value_sett &_value_set, const 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 SSA_stept & SSA_step
 
const goto_symex_statet & s
 

Detailed Description

Definition at line 24 of file postcondition.cpp.

Constructor & Destructor Documentation

◆ postconditiont()

postconditiont::postconditiont ( const namespacet &  _ns,
const value_sett &  _value_set,
const SSA_stept &  _SSA_step,
const goto_symex_statet &  _s 
)
inline

Definition at line 27 of file postcondition.cpp.

Member Function Documentation

◆ compute()

void postconditiont::compute ( exprt &  dest)

Definition at line 96 of file postcondition.cpp.

◆ is_used()

bool postconditiont::is_used ( const exprt &  expr,
const irep_idt &  identifier 
)
protected

Definition at line 148 of file postcondition.cpp.

◆ is_used_address_of()

bool postconditiont::is_used_address_of ( const exprt &  expr,
const irep_idt &  identifier 
)
protected

Definition at line 71 of file postcondition.cpp.

◆ strengthen()

void postconditiont::strengthen ( exprt &  dest)
protected

Definition at line 127 of file postcondition.cpp.

◆ weaken()

void postconditiont::weaken ( exprt &  dest)
protected

Definition at line 105 of file postcondition.cpp.

Member Data Documentation

◆ ns

const namespacet& postconditiont::ns
protected

Definition at line 37 of file postcondition.cpp.

◆ s

const goto_symex_statet& postconditiont::s
protected

Definition at line 40 of file postcondition.cpp.

◆ SSA_step

const SSA_stept& postconditiont::SSA_step
protected

Definition at line 39 of file postcondition.cpp.

◆ value_set

const value_sett& postconditiont::value_set
protected

Definition at line 38 of file postcondition.cpp.

The documentation for this class was generated from the following file: