cprover
|
Public Member Functions | |
contract_clausest (const exprt::operandst &decreases) | |
Public Attributes | |
exprt | invariant_expr |
assignst | assigns |
exprt::operandst | decreases_clauses |
Definition at line 315 of file dfcc_cfg_info.cpp.
|
inlineexplicit |
Definition at line 317 of file dfcc_cfg_info.cpp.
assignst contract_clausest::assigns |
Definition at line 322 of file dfcc_cfg_info.cpp.
exprt::operandst contract_clausest::decreases_clauses |
Definition at line 323 of file dfcc_cfg_info.cpp.
exprt contract_clausest::invariant_expr |
Definition at line 321 of file dfcc_cfg_info.cpp.