CBMC
|
Public Member Functions | |
contract_clausest (const exprt::operandst &decreases) | |
Public Attributes | |
exprt | invariant_expr |
assignst | assigns |
exprt::operandst | decreases_clauses |
Definition at line 295 of file dfcc_cfg_info.cpp.
|
inlineexplicit |
Definition at line 297 of file dfcc_cfg_info.cpp.
assignst contract_clausest::assigns |
Definition at line 302 of file dfcc_cfg_info.cpp.
exprt::operandst contract_clausest::decreases_clauses |
Definition at line 303 of file dfcc_cfg_info.cpp.
exprt contract_clausest::invariant_expr |
Definition at line 301 of file dfcc_cfg_info.cpp.