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/c_types.h>
#include <util/message.h>
#include <util/namespace.h>
#include <util/pointer_expr.h>
#include <util/replace_symbol.h>
Go to the source code of this file.
Classes | |
class | code_contractst |
class | assigns_clause_targett |
A base class for assigns clause targets. More... | |
class | assigns_clause_scalar_targett |
class | assigns_clause_struct_targett |
class | assigns_clause_array_targett |
class | assigns_clauset |
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 200 of file code_contracts.h.
#define FLAG_ENFORCE_CONTRACT "enforce-contract" |
Definition at line 196 of file code_contracts.h.
#define FLAG_REPLACE_ALL_CALLS "replace-all-calls-with-contracts" |
Definition at line 191 of file code_contracts.h.
#define FLAG_REPLACE_CALL "replace-call-with-contract" |
Definition at line 186 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 201 of file code_contracts.h.
#define HELP_ENFORCE_CONTRACT " --enforce-contract <fun> wrap fun with an assertion of its contract\n" |
Definition at line 197 of file code_contracts.h.
#define HELP_REPLACE_ALL_CALLS |
Definition at line 192 of file code_contracts.h.
#define HELP_REPLACE_CALL |
Definition at line 187 of file code_contracts.h.