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

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
 

Detailed Description

Definition at line 22 of file precondition.cpp.

Constructor & Destructor Documentation

◆ preconditiont()

preconditiont::preconditiont ( const namespacet &  _ns,
value_setst &  _value_sets,
const goto_programt::const_targett  _target,
const SSA_stept &  _SSA_step,
const goto_symex_statet &  _s 
)
inline

Definition at line 25 of file precondition.cpp.

Member Function Documentation

◆ compute()

void preconditiont::compute ( exprt &  dest)

Definition at line 96 of file precondition.cpp.

◆ compute_address_of()

void preconditiont::compute_address_of ( exprt &  dest)
protected

Definition at line 74 of file precondition.cpp.

◆ compute_rec()

void preconditiont::compute_rec ( exprt &  dest)
protected

Definition at line 101 of file precondition.cpp.

Member Data Documentation

◆ ns

const namespacet& preconditiont::ns
protected

Definition at line 40 of file precondition.cpp.

◆ s

const goto_symex_statet& preconditiont::s
protected

Definition at line 44 of file precondition.cpp.

◆ SSA_step

const SSA_stept& preconditiont::SSA_step
protected

Definition at line 43 of file precondition.cpp.

◆ target

const goto_programt::const_targett preconditiont::target
protected

Definition at line 42 of file precondition.cpp.

◆ value_sets

value_setst& preconditiont::value_sets
protected

Definition at line 41 of file precondition.cpp.

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