cprover
|
Verify and use annotated invariants and pre/post-conditions. More...
#include <set>
#include <string>
#include <unordered_set>
#include <goto-programs/goto_functions.h>
#include <goto-programs/goto_model.h>
#include <util/namespace.h>
Go to the source code of this file.
Classes | |
class | code_contractst |
Macros | |
#define | FLAG_REPLACE_CALL "replace-call-with-contract" |
#define | HELP_REPLACE_CALL |
#define | FLAG_REPLACE_ALL_CALLS "replace-all-calls-with-contracts" |
#define | HELP_REPLACE_ALL_CALLS |
#define | FLAG_ENFORCE_CONTRACT "enforce-contract" |
#define | HELP_ENFORCE_CONTRACT " --enforce-contract <fun> wrap fun with an assertion of its contract\n" |
#define | FLAG_ENFORCE_ALL_CONTRACTS "enforce-all-contracts" |
#define | HELP_ENFORCE_ALL_CONTRACTS " --enforce-all-contracts as above for all functions with a contract\n" |
Verify and use annotated invariants and pre/post-conditions.
Definition in file code_contracts.h.
#define FLAG_ENFORCE_ALL_CONTRACTS "enforce-all-contracts" |
Definition at line 168 of file code_contracts.h.
#define FLAG_ENFORCE_CONTRACT "enforce-contract" |
Definition at line 164 of file code_contracts.h.
#define FLAG_REPLACE_ALL_CALLS "replace-all-calls-with-contracts" |
Definition at line 159 of file code_contracts.h.
#define FLAG_REPLACE_CALL "replace-call-with-contract" |
Definition at line 154 of file code_contracts.h.
#define HELP_ENFORCE_ALL_CONTRACTS " --enforce-all-contracts as above for all functions with a contract\n" |
Definition at line 169 of file code_contracts.h.
#define HELP_ENFORCE_CONTRACT " --enforce-contract <fun> wrap fun with an assertion of its contract\n" |
Definition at line 165 of file code_contracts.h.
#define HELP_REPLACE_ALL_CALLS |
Definition at line 160 of file code_contracts.h.
#define HELP_REPLACE_CALL |
Definition at line 155 of file code_contracts.h.