31 const symbolt &pure_contract_symbol,
38 : pure_contract_symbol(pure_contract_symbol),
40 spec_assigns_function_id(
41 id2string(pure_contract_symbol.name) +
"::assigns"),
42 spec_assigns_havoc_function_id(
43 id2string(pure_contract_symbol.name) +
"::assigns::havoc"),
44 spec_frees_function_id(
id2string(pure_contract_symbol.name) +
"::frees"),
45 language_mode(pure_contract_symbol.mode),
46 goto_model(goto_model),
47 message_handler(message_handler),
50 spec_functions(spec_functions),
51 contract_clauses_codegen(contract_clauses_codegen),
52 instrument(instrument),
53 ns(goto_model.symbol_table)
81 std::set<irep_idt> function_pointer_contracts;
86 function_pointer_contracts.empty(),
126 const auto &spec_function_id = spec_function_symbol.name;
128 auto &spec_code_type =
to_code_type(spec_function_symbol.type);
136 lambda_parameters.push_back(
140 for(
const auto ¶m_id : spec_code_type.parameter_identifiers())
142 lambda_parameters.push_back(
ns.
lookup(param_id).symbol_expr());
155 targets.push_back(new_target);
160 spec_function_symbol.mode, targets, body);
178 const auto &spec_function_id = spec_function_symbol.name;
180 auto &spec_code_type =
to_code_type(spec_function_symbol.type);
189 dummy.
name =
"dummy_return_value";
194 for(
const auto ¶m_id : spec_code_type.parameter_identifiers())
196 lambda_parameters.push_back(
ns.
lookup(param_id).symbol_expr());
209 targets.push_back(new_target);
214 spec_function_symbol.mode, targets, body);
API to expression classes that are internal to the C frontend.
const code_with_contract_typet & to_code_with_contract_type(const typet &type)
Cast a typet to a code_with_contract_typet.
const typet & return_type() const
const exprt::operandst & c_assigns() const
const exprt::operandst & c_frees() const
Translates assigns and frees clauses of a function contract or loop contract into GOTO programs that ...
void gen_spec_assigns_instructions(const irep_idt &language_mode, const exprt::operandst &assigns_clause, goto_programt &dest)
Generates instructions encoding the assigns_clause targets and adds them to dest.
void gen_spec_frees_instructions(const irep_idt &language_mode, const exprt::operandst &frees_clause, goto_programt &dest)
Generates instructions encoding the frees_clause targets and adds them to dest.
void gen_spec_frees_function()
Translates the contract's frees clause to a GOTO function that uses the freeable built-in to express ...
std::size_t nof_assigns_targets
const irep_idt spec_assigns_havoc_function_id
Identifier of the contract::c_assigns::havoc function.
dfcc_instrumentt & instrument
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.
std::size_t nof_frees_targets
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 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 ...
void instrument_function(const irep_idt &function_id, const loop_contract_configt &loop_contract_config, std::set< irep_idt > &function_pointer_contracts)
Instruments a GOTO function by adding an extra write set parameter and instrumenting its body instruc...
Class interface to library types and functions defined in cprover_contracts.c.
This class rewrites GOTO functions that use the built-ins:
void to_spec_assigns_function(const irep_idt &function_id, std::size_t &nof_targets)
Transforms (in place) a function.
void generate_havoc_function(const irep_idt &function_id, const irep_idt &havoc_function_id, std::size_t &nof_targets)
From a function:
void to_spec_frees_function(const irep_idt &function_id, std::size_t &nof_targets)
Transforms (in place) a function.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
std::vector< exprt > operandst
source_locationt & add_source_location()
function_mapt function_map
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
goto_functionst goto_functions
GOTO functions.
A generic container class for the GOTO intermediate representation of one function.
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
targett add(instructiont &&instruction)
Adds a given instruction at the end.
const irep_idt & id() const
exprt application(const operandst &arguments) const
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Expression to hold a symbol (variable)
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
typet type
Type of symbol.
irep_idt name
The unique identifier.
Translates assigns and frees clauses of a function contract or loop contract into goto programs that ...
Translates assigns and frees clauses of a function contract into goto functions that allow to build a...
Add instrumentation to a goto program to perform frame condition checks.
Dynamic frame condition checking library loading.
Translate functions that specify assignable and freeable targets declaratively into active functions ...
Deprecated expression utility functions.
Fresh auxiliary symbol creation.
const std::string & id2string(const irep_idt &d)
API to expression classes for 'mathematical' expressions.
const lambda_exprt & to_lambda_expr(const exprt &expr)
Cast an exprt to a lambda_exprt.
API to expression classes.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
static const symbolt & clone_and_rename_function(goto_modelt &goto_model, const irep_idt &function_id, const irep_idt &new_function_id, std::optional< typet > new_return_type)
Creates a new function symbol and goto_function entry in the goto_functions_map by cloning the given ...
Loop contract configurations.