CBMC
dfcc_contract_functions.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Dynamic frame condition checking for function contracts
4 
5 Author: Remi Delmas, delmasrd@amazon.com
6 Date: August 2022
7 
8 \*******************************************************************/
9 
13 
14 #ifndef CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_CONTRACT_FUNCTIONS_H
15 #define CPROVER_GOTO_INSTRUMENT_CONTRACTS_DYNAMIC_FRAMES_DFCC_CONTRACT_FUNCTIONS_H
16 
18 
19 #include <util/message.h>
20 #include <util/namespace.h>
21 #include <util/std_expr.h>
22 
23 #include "dfcc_contract_mode.h"
24 
25 #include <set>
26 
27 class goto_modelt;
28 class message_handlert;
29 class dfcc_libraryt;
30 class dfcc_instrumentt;
35 
64 {
65 public:
82 
86  const irep_idt &spec_function_id);
87 
90 
93 
96 
98  const std::size_t get_nof_assigns_targets() const;
99 
101  const std::size_t get_nof_frees_targets() const;
102 
105 
108 
111 
114 
117 
120 
121 protected:
130  std::size_t nof_assigns_targets;
131  std::size_t nof_frees_targets;
132 
137 
141 };
142 
143 #endif
A class for an expression that represents a conditional target or a list of targets sharing a common ...
Definition: c_expr.h:233
Translates assigns and frees clauses of a function contract or loop contract into GOTO programs that ...
Generates GOTO functions modelling a contract assigns and frees clauses.
void gen_spec_frees_function()
Translates the contract's frees clause to a GOTO function that uses the freeable built-in to express ...
const irep_idt spec_assigns_havoc_function_id
Identifier of the contract::c_assigns::havoc function.
const code_with_contract_typet & code_with_contract
The code_with_contract_type carrying the contract clauses.
const symbolt & get_spec_frees_function_symbol() const
Returns the contract::frees function symbol.
dfcc_contract_clauses_codegent & contract_clauses_codegen
const irep_idt spec_assigns_function_id
Identifier of the contract::c_assigns function.
void instrument_without_loop_contracts_check_no_pointer_contracts(const irep_idt &spec_function_id)
Instruments the given function without loop contracts and checks that no function pointer contracts w...
dfcc_contract_functionst(const symbolt &pure_contract_symbol, goto_modelt &goto_model, message_handlert &message_handler, dfcc_libraryt &library, dfcc_spec_functionst &spec_functions, dfcc_contract_clauses_codegent &contract_clauses_codegen, dfcc_instrumentt &instrument)
const symbolt & get_spec_assigns_function_symbol() const
Returns the contract::c_assigns function symbol.
const symbolt & pure_contract_symbol
The function symbol carrying the contract.
const std::size_t get_nof_assigns_targets() const
Returns the maximum number of targets in the assigns clause.
const symbolt & get_spec_assigns_havoc_function_symbol() const
Returns the contract::c_assigns::havoc function symbol.
void gen_spec_assigns_function()
Translates the contract's assigns clause to a GOTO function that uses the assignable,...
const irep_idt spec_frees_function_id
Identifier of the contract::frees function.
dfcc_spec_functionst & spec_functions
const irep_idt & language_mode
Language mode of the contract symbol.
const std::size_t get_nof_frees_targets() const
Returns the maximum number of targets in the frees clause.
This class instruments GOTO functions or instruction sequences for frame condition checking and loop ...
Class interface to library types and functions defined in cprover_contracts.c.
Definition: dfcc_library.h:154
This class rewrites GOTO functions that use the built-ins:
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:154
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
Symbol table entry.
Definition: symbol.h:28
Enum type representing the contract checking and replacement modes.
Program Transformation.
API to expression classes.