contract_clausest Struct Reference

Collaboration diagram for contract_clausest:

Public Member Functions
	contract_clausest (const exprt::operandst &decreases)

Public Attributes
exprt	invariant_expr
assignst	assigns
exprt::operandst	decreases_clauses

Detailed Description

Definition at line 295 of file dfcc_cfg_info.cpp.

Constructor & Destructor Documentation

contract_clausest()

contract_clausest::contract_clausest ( const exprt::operandst &  decreases )

inlineexplicit

Definition at line 297 of file dfcc_cfg_info.cpp.

Member Data Documentation

assigns

assignst contract_clausest::assigns

Definition at line 302 of file dfcc_cfg_info.cpp.

decreases_clauses

exprt::operandst contract_clausest::decreases_clauses

Definition at line 303 of file dfcc_cfg_info.cpp.

invariant_expr

exprt contract_clausest::invariant_expr

Definition at line 301 of file dfcc_cfg_info.cpp.

---

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

• /home/runner/work/cbmc/cbmc/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp