#include <goto-programs/goto_convert_class.h>#include <util/message.h>#include <util/namespace.h>#include <util/optional.h>#include <util/pointer_expr.h>#include <goto-programs/goto_functions.h>#include <goto-programs/goto_model.h>#include <goto-programs/instrument_preconditions.h>#include <goto-instrument/loop_utils.h>#include <list>#include <map>#include <set>#include <string>#include <unordered_set>
Include dependency graph for contracts.h: This graph shows which files directly or indirectly include this file:Go to the source code of this file.
Classes | |
| class | code_contractst |
Macros | |
| #define | FLAG_LOOP_CONTRACTS "apply-loop-contracts" |
| #define | HELP_LOOP_CONTRACTS |
| #define | FLAG_REPLACE_CALL "replace-call-with-contract" |
| #define | HELP_REPLACE_CALL |
| #define | FLAG_ENFORCE_CONTRACT "enforce-contract" |
| #define | HELP_ENFORCE_CONTRACT " --enforce-contract <fun> wrap fun with an assertion of its contract\n" |
Detailed Description
Verify and use annotated invariants and pre/post-conditions
Definition in file contracts.h.
Macro Definition Documentation
◆ FLAG_ENFORCE_CONTRACT
| #define FLAG_ENFORCE_CONTRACT "enforce-contract" |
Definition at line 46 of file contracts.h.
◆ FLAG_LOOP_CONTRACTS
| #define FLAG_LOOP_CONTRACTS "apply-loop-contracts" |
Definition at line 36 of file contracts.h.
◆ FLAG_REPLACE_CALL
| #define FLAG_REPLACE_CALL "replace-call-with-contract" |
Definition at line 41 of file contracts.h.
◆ HELP_ENFORCE_CONTRACT
| #define HELP_ENFORCE_CONTRACT " --enforce-contract <fun> wrap fun with an assertion of its contract\n" |
Definition at line 47 of file contracts.h.
◆ HELP_LOOP_CONTRACTS
| #define HELP_LOOP_CONTRACTS |
Value:
" --apply-loop-contracts\n" \
" check and use loop contracts when provided\n"
Definition at line 37 of file contracts.h.
◆ HELP_REPLACE_CALL
| #define HELP_REPLACE_CALL |
Value:
" --replace-call-with-contract <fun>\n" \
" replace calls to fun with fun's contract\n"
Definition at line 42 of file contracts.h.
