35 std::map<irep_idt, dfcc_contract_functionst>
46 : goto_model(goto_model),
47 message_handler(message_handler),
50 instrument(instrument),
51 memory_predicates(memory_predicates),
52 spec_functions(spec_functions),
53 contract_clauses_codegen(contract_clauses_codegen),
54 ns(goto_model.symbol_table)
93 const symbolt &wrapper_write_set_symbol,
95 std::set<irep_idt> &function_pointer_contracts)
102 wrapper_write_set_symbol,
113 const std::optional<irep_idt> function_id_opt)
115 auto pure_contract_id =
"contract::" +
id2string(contract_id);
116 const symbolt *pure_contract_symbol =
nullptr;
117 if(!
ns.
lookup(pure_contract_id, pure_contract_symbol))
119 if(function_id_opt.has_value())
121 auto function_id = function_id_opt.
value();
122 const auto &function_symbol =
130 return *pure_contract_symbol;
138 function_id_opt.has_value(),
139 "Contract '" + pure_contract_id +
140 "' not found, the identifier of an existing function must be provided "
141 "to derive a default contract");
143 auto function_id = function_id_opt.value();
144 const auto &function_symbol =
148 <<
"' not found, deriving empty pure contract '"
149 << pure_contract_id <<
"' from function '" << function_id
153 pure_contract_id, function_symbol.
type, function_symbol.mode};
154 new_symbol.base_name = pure_contract_id;
155 new_symbol.pretty_name = pure_contract_id;
156 new_symbol.is_property =
true;
157 new_symbol.module = function_symbol.module;
158 new_symbol.location = function_symbol.location;
162 "contract '" +
id2string(function_symbol.display_name()) +
163 "' already set at " +
id2string(entry.first.location.as_string()));
166 ns.
lookup(pure_contract_id, pure_contract_symbol);
167 return *pure_contract_symbol;
183 std::ostringstream err_msg;
184 err_msg <<
"dfcc_contract_handlert: function '" << contract_id
185 <<
"' and the corresponding pure contract symbol '"
186 << pure_contract_id <<
"' have incompatible type signatures:\n";
188 err_msg <<
"- contract return type "
191 for(
const auto ¶m : contract_type.
parameters())
193 err_msg <<
"- contract param type "
194 <<
from_type(
ns, contract_id, param.type()) <<
"\n";
197 err_msg <<
"- pure contract return type "
201 for(
const auto ¶m : pure_contract_type.
parameters())
203 err_msg <<
"- pure contract param type "
204 <<
from_type(
ns, pure_contract_id, param.type()) <<
"\n";
207 err_msg <<
"aborting."
API to expression classes that are internal to the C frontend.
const typet & return_type() const
const parameterst & parameters() const
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.
const std::size_t get_nof_assigns_targets() const
Returns the maximum number of targets in the assigns clause.
void check_signature_compat(const irep_idt &contract_id, const code_typet &contract_type, const irep_idt &pure_contract_id, const code_typet &pure_contract_type)
Throws an error if the type signatures are not compatible.
dfcc_spec_functionst & spec_functions
const symbolt & get_pure_contract_symbol(const irep_idt &contract_id, const std::optional< irep_idt > function_id_opt={})
Searches for a symbol named "contract::contract_id" in the symbol table.
static std::map< irep_idt, dfcc_contract_functionst > contract_cache
dfcc_lift_memory_predicatest & memory_predicates
message_handlert & message_handler
dfcc_contract_clauses_codegent & contract_clauses_codegen
const std::size_t get_assigns_clause_size(const irep_idt &contract_id)
Returns the size assigns clause of the given contract in number of targets.
void add_contract_instructions(const dfcc_contract_modet contract_mode, const irep_idt &wrapper_id, const irep_idt &wrapped_id, const irep_idt &contract_id, const symbolt &wrapper_write_set_symbol, goto_programt &dest, std::set< irep_idt > &function_pointer_contracts)
Adds instructions in dest modeling contract checking, assuming that ret_t wrapper_id(params) is the f...
dfcc_instrumentt & instrument
dfcc_contract_handlert(goto_modelt &goto_model, message_handlert &message_handler, dfcc_libraryt &library, dfcc_instrumentt &instrument, dfcc_lift_memory_predicatest &memory_predicates, dfcc_spec_functionst &spec_functions, dfcc_contract_clauses_codegent &contract_clauses_codegen)
const dfcc_contract_functionst & get_contract_functions(const irep_idt &contract_id)
Returns the dfcc_contract_functionst object for the given contract from the cache,...
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:
Generates the body of a wrapper function from a contract specified using requires,...
void add_to_dest(goto_programt &dest, std::set< irep_idt > &dest_fp_contracts)
Adds the whole program to dest and the discovered function pointer contracts dest_fp_contracts.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
symbol_tablet symbol_table
Symbol table.
A generic container class for the GOTO intermediate representation of one function.
Thrown when we can't handle something in an input source file.
mstreamt & warning() const
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
virtual std::pair< symbolt &, bool > insert(symbolt symbol) override
Author: Diffblue Ltd.
typet type
Type of symbol.
exprt value
Initial value of symbol.
const source_locationt & source_location() const
Specialisation of dfcc_contract_handlert for contracts.
dfcc_contract_modet
Enum type representing the contract checking and replacement modes.
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 ...
Generates the body of a wrapper function from a contract for contract checking or contract replacemen...
Deprecated expression utility functions.
Fresh auxiliary symbol creation.
const std::string & id2string(const irep_idt &d)
std::string from_type(const namespacet &ns, const irep_idt &identifier, const typet &type)
API to expression classes for 'mathematical' expressions.
bool function_is_type_compatible(bool return_value_used, const code_typet &call_type, const code_typet &function_type, const namespacet &ns)
Returns true iff call_type can be converted to produce a function call of the same type as function_t...
Remove Indirect Function Calls.
#define PRECONDITION_WITH_DIAGNOSTICS(CONDITION,...)
API to expression classes.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
static symbolt & get_function_symbol(symbol_table_baset &, const irep_idt &function_id)
Returns the symbolt for function_id.