cprover
code_contracts.h File Reference

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>
+ Include dependency graph for code_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_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"
 

Detailed Description

Verify and use annotated invariants and pre/post-conditions.

Definition in file code_contracts.h.

Macro Definition Documentation

◆ FLAG_ENFORCE_ALL_CONTRACTS

#define FLAG_ENFORCE_ALL_CONTRACTS   "enforce-all-contracts"

Definition at line 168 of file code_contracts.h.

◆ FLAG_ENFORCE_CONTRACT

#define FLAG_ENFORCE_CONTRACT   "enforce-contract"

Definition at line 164 of file code_contracts.h.

◆ FLAG_REPLACE_ALL_CALLS

#define FLAG_REPLACE_ALL_CALLS   "replace-all-calls-with-contracts"

Definition at line 159 of file code_contracts.h.

◆ FLAG_REPLACE_CALL

#define FLAG_REPLACE_CALL   "replace-call-with-contract"

Definition at line 154 of file code_contracts.h.

◆ HELP_ENFORCE_ALL_CONTRACTS

#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.

◆ HELP_ENFORCE_CONTRACT

#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.

◆ HELP_REPLACE_ALL_CALLS

#define HELP_REPLACE_ALL_CALLS
Value:
" --replace-all-calls-with-contracts\n" \
" as above for all functions with a contract\n"

Definition at line 160 of file code_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 155 of file code_contracts.h.