Loading...

Searching...

No Matches

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 23 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 26 of file postcondition.cpp.

Member Function Documentation

◆ compute()

void postconditiont::compute ( exprt & dest )

Definition at line 95 of file postcondition.cpp.

◆ is_used()

bool postconditiont::is_used ( const exprt & expr,

const irep_idt & identifier

)

protected

Definition at line 147 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 70 of file postcondition.cpp.

◆ strengthen()

void postconditiont::strengthen ( exprt & dest )

protected

Definition at line 126 of file postcondition.cpp.

◆ weaken()

void postconditiont::weaken ( exprt & dest )

protected

Definition at line 104 of file postcondition.cpp.

Member Data Documentation

◆ ns

const namespacet& postconditiont::ns

protected

Definition at line 36 of file postcondition.cpp.

◆ s

const goto_symex_statet& postconditiont::s

protected

Definition at line 39 of file postcondition.cpp.

◆ SSA_step

const SSA_stept& postconditiont::SSA_step

protected

Definition at line 38 of file postcondition.cpp.

◆ value_set

const value_sett& postconditiont::value_set

protected

Definition at line 37 of file postcondition.cpp.

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

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