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/c_types.h>
#include <util/message.h>
#include <util/namespace.h>
#include <util/pointer_expr.h>
#include <util/replace_symbol.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
 
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"
 

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 200 of file code_contracts.h.

◆ FLAG_ENFORCE_CONTRACT

#define FLAG_ENFORCE_CONTRACT   "enforce-contract"

Definition at line 196 of file code_contracts.h.

◆ FLAG_REPLACE_ALL_CALLS

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

Definition at line 191 of file code_contracts.h.

◆ FLAG_REPLACE_CALL

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

Definition at line 186 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 201 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 197 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 192 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 187 of file code_contracts.h.