55 gen_spec_assigns_function();
81 std::set<irep_idt> function_pointer_contracts;
86 function_pointer_contracts.empty(),
118void dfcc_contract_functionst::gen_spec_assigns_function()
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());
146 goto_functiont &goto_function =
147 goto_model.goto_functions.function_map.at(spec_function_id);
155 targets.push_back(new_target);
158 goto_programt &body = goto_function.
body;
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());
201 goto_model.goto_functions.function_map.at(spec_function_id);
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
Translates assigns and frees clauses of a function contract or loop contract into GOTO programs that ...
void gen_spec_frees_function()
Translates the contract's assigns clause to a GOTO function that uses the assignable,...
std::size_t nof_assigns_targets
const irep_idt spec_assigns_havoc_function_id
Identifier of the contract::c_assigns::havoc function.
message_handlert & message_handler
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.
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.
This class rewrites GOTO functions that use the built-ins:
Base class for all expressions.
std::vector< exprt > operandst
source_locationt & add_source_location()
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
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
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.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
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.