Loading...

Searching...

No Matches

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, message_handlert &message_handler)

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

message_handlert & message_handler

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,

message_handlert & message_handler

)

inline

Definition at line 25 of file precondition.cpp.

Member Function Documentation

◆ compute()

void preconditiont::compute ( exprt & dest )

Definition at line 100 of file precondition.cpp.

◆ compute_address_of()

void preconditiont::compute_address_of ( exprt & dest )

protected

Definition at line 78 of file precondition.cpp.

◆ compute_rec()

void preconditiont::compute_rec ( exprt & dest )

protected

Definition at line 105 of file precondition.cpp.

Member Data Documentation

◆ message_handler

message_handlert& preconditiont::message_handler

protected

Definition at line 47 of file precondition.cpp.

◆ ns

const namespacet& preconditiont::ns

protected

Definition at line 42 of file precondition.cpp.

◆ s

const goto_symex_statet& preconditiont::s

protected

Definition at line 46 of file precondition.cpp.

◆ SSA_step

const SSA_stept& preconditiont::SSA_step

protected

Definition at line 45 of file precondition.cpp.

◆ target

const goto_programt::const_targett preconditiont::target

protected

Definition at line 44 of file precondition.cpp.

◆ value_sets

value_setst& preconditiont::value_sets

protected

Definition at line 43 of file precondition.cpp.

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

/home/runner/work/cbmc/cbmc/src/goto-symex/precondition.cpp