CBMC
Public Member Functions | Public Attributes | List of all members
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 334 of file dfcc_cfg_info.cpp.

Constructor & Destructor Documentation

◆ contract_clausest()

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

Definition at line 336 of file dfcc_cfg_info.cpp.

Member Data Documentation

◆ assigns

assignst contract_clausest::assigns

Definition at line 341 of file dfcc_cfg_info.cpp.

◆ decreases_clauses

exprt::operandst contract_clausest::decreases_clauses

Definition at line 342 of file dfcc_cfg_info.cpp.

◆ invariant_expr

exprt contract_clausest::invariant_expr

Definition at line 340 of file dfcc_cfg_info.cpp.

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