cprover
preconditiont Class Reference
Collaboration diagram for preconditiont:
[legend]

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 namespacetns
 
value_setstvalue_sets
 
const goto_programt::const_targett target
 
const symex_target_equationt::SSA_steptSSA_step
 
const goto_symex_statets
 

Detailed Description

Definition at line 20 of file precondition.cpp.

Constructor & Destructor Documentation

§ preconditiont()

preconditiont::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 
)
inline

Definition at line 23 of file precondition.cpp.

Member Function Documentation

§ compute()

void preconditiont::compute ( exprt dest)

Definition at line 96 of file precondition.cpp.

References compute_rec().

Referenced by compute_address_of(), and precondition().

§ compute_address_of()

void preconditiont::compute_address_of ( exprt dest)
protected

Definition at line 72 of file precondition.cpp.

References compute(), irept::id(), exprt::op0(), exprt::op1(), and exprt::operands().

Referenced by compute_rec().

§ compute_rec()

Member Data Documentation

§ ns

const namespacet& preconditiont::ns
protected

Definition at line 38 of file precondition.cpp.

Referenced by compute_rec().

§ s

const goto_symex_statet& preconditiont::s
protected

Definition at line 42 of file precondition.cpp.

Referenced by compute_rec().

§ SSA_step

const symex_target_equationt::SSA_stept& preconditiont::SSA_step
protected

Definition at line 41 of file precondition.cpp.

Referenced by compute_rec().

§ target

const goto_programt::const_targett preconditiont::target
protected

Definition at line 40 of file precondition.cpp.

Referenced by compute_rec().

§ value_sets

value_setst& preconditiont::value_sets
protected

Definition at line 39 of file precondition.cpp.

Referenced by compute_rec().


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