26 : goto_model(goto_model),
27 message_handler(message_handler),
30 ns(goto_model.symbol_table)
37 expr.
id() == ID_typecast && expr.
type().
id() == ID_pointer &&
38 expr.
operands().at(0).id() == ID_address_of,
39 "target expression must be of the form `cast(address_of(target), empty*)`");
41 return expr.
operands().at(0).operands().at(0).type();
47 std::size_t &nof_targets)
51 "DFCC: havoc function id '" +
id2string(havoc_function_id) +
54 const auto &function_symbol =
58 const typet &write_set_param_type =
65 havoc_function_symbol.
base_name = havoc_function_id;
66 havoc_function_symbol.name = havoc_function_id;
67 havoc_function_symbol.pretty_name = havoc_function_id;
68 havoc_function_symbol.type = havoc_code_type;
69 havoc_function_symbol.mode = function_symbol.mode;
70 havoc_function_symbol.module = function_symbol.module;
71 havoc_function_symbol.location = function_symbol.location;
72 havoc_function_symbol.set_compiled();
76 "DFCC: could not insert havoc function '" +
id2string(havoc_function_id) +
77 "' in the symbol table");
83 "__write_set_to_havoc",
84 write_set_param_type);
88 .set_identifier(write_set_symbol.name);
94 dummy_havoc_function);
106 write_set_symbol.symbol_expr(),
114 std::set<irep_idt> no_body;
115 std::set<irep_idt> missing_function;
116 std::set<irep_idt> recursive_call;
117 std::set<irep_idt> not_enough_arguments;
124 not_enough_arguments,
128 "no body warnings when inlining " +
id2string(havoc_function_id));
130 missing_function.empty(),
131 "missing function warnings when inlining " +
id2string(havoc_function_id));
133 recursive_call.empty(),
134 "recursive calls when inlining " +
id2string(havoc_function_id));
136 not_enough_arguments.empty(),
137 "not enough arguments when inlining " +
id2string(havoc_function_id));
147 const exprt &write_set_to_havoc,
149 std::size_t &nof_targets)
152 std::size_t next_idx = 0;
158 if(ins_it->is_function_call())
160 if(ins_it->call_function().id() != ID_symbol)
163 "Function pointer calls are not supported in assigns clauses: '" +
164 from_expr(
ns, function_id, ins_it->call_function()) +
165 "' called in function '" +
id2string(function_id) +
"'",
166 ins_it->source_location());
178 hook_opt.has_value(),
179 "dfcc_spec_functionst::generate_havoc_instructions: function calls "
180 "must be inlined before calling this function");
184 auto hook = hook_opt.value();
187 {write_set_to_havoc, from_integer(next_idx, size_type())});
210 call.
lhs() = target_expr;
213 auto goto_instruction =
226 goto_instruction->complete_goto(label);
244 nof_targets = next_idx;
249 std::size_t &nof_targets)
254 const exprt write_set_to_fill =
258 "__write_set_to_fill",
274 const exprt &write_set_to_fill,
277 std::size_t &nof_targets)
281 std::size_t next_idx = 0;
286 if(ins_it->is_function_call())
288 if(ins_it->call_function().id() != ID_symbol)
291 "Function pointer calls are not supported in assigns clauses '" +
294 ins_it->source_location());
306 "dfcc_spec_functionst::to_spec_assigns_function: function calls must "
307 "be inlined before calling this function");
313 ins_it->call_arguments().insert(
316 ins_it->call_arguments().insert(
317 ins_it->call_arguments().begin(), write_set_to_fill);
322 ins_it->call_arguments().pop_back();
327 nof_targets = next_idx;
332 std::size_t &nof_targets)
337 const exprt &write_set_to_fill =
341 "__write_set_to_fill",
357 const exprt &write_set_to_fill,
360 std::size_t &nof_targets)
363 std::size_t next_idx = 0;
366 if(ins_it->is_function_call())
368 if(ins_it->call_function().id() != ID_symbol)
371 "Function pointer calls are not supported in frees clauses: '" +
374 ins_it->source_location());
384 "dfcc_spec_functionst::to_spec_frees_function: function calls must "
385 "be inlined before calling this function");
387 ins_it->call_function() =
390 ins_it->call_arguments().insert(
391 ins_it->call_arguments().begin(), write_set_to_fill);
396 nof_targets = next_idx;
unsignedbv_typet size_type()
pointer_typet pointer_type(const typet &subtype)
goto_instruction_codet representation of a function call statement.
const parameterst & parameters() const
Operator to dereference a pointer.
Class interface to library types and functions defined in cprover_contracts.c.
bool is_front_end_builtin(const irep_idt &function_id) const
Returns true iff the given function_id is one of __CPROVER_assignable, __CPROVER_object_whole,...
dfcc_funt get_hook(const irep_idt &function_id) const
Returns the library instrumentation hook for the given front-end function.
std::map< dfcc_typet, typet > dfcc_type
Maps enum values to the actual types (dynamically loaded)
optionalt< dfcc_funt > get_havoc_hook(const irep_idt &function_id) const
Returns the library instrumentation hook for the given built-in.
std::map< dfcc_funt, symbolt > dfcc_fun_symbol
Maps enum values to the actual function symbols (dynamically loaded)
void to_spec_assigns_function(const irep_idt &function_id, std::size_t &nof_targets)
Transforms (in place) a function.
void to_spec_frees_instructions(const exprt &write_set_to_fill, const irep_idt &language_mode, goto_programt &program, std::size_t &nof_targets)
Rewrites in place program expressed in terms of built-ins specifying freeable targets declaratively u...
void generate_havoc_function(const irep_idt &function_id, const irep_idt &havoc_function_id, std::size_t &nof_targets)
From a function:
void generate_havoc_instructions(const irep_idt &function_id, const goto_programt &original_program, const exprt &write_set_to_havoc, goto_programt &havoc_program, std::size_t &nof_targets)
Translates original_program that specifies assignable targets into a program that havocs the targets.
message_handlert & message_handler
void to_spec_assigns_instructions(const exprt &write_set_to_fill, const irep_idt &language_mode, goto_programt &program, std::size_t &nof_targets)
Rewrites in place program expressed in terms of built-ins specifying assignable targets declaratively...
const typet & get_target_type(const exprt &expr)
Extracts the type of an assigns clause target expression The expression must be of the form: expr = c...
dfcc_spec_functionst(goto_modelt &goto_model, message_handlert &message_handler, dfcc_libraryt &library)
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.
typet & type()
Return the type of the expression.
function_mapt function_map
A goto function, consisting of function body (see body) and parameter identifiers (see parameter_iden...
parameter_identifierst parameter_identifiers
The identifiers of the parameters of this function.
symbol_tablet symbol_table
Symbol table.
goto_functionst goto_functions
GOTO functions.
A generic container class for the GOTO intermediate representation of one function.
static instructiont make_dead(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
static instructiont make_end_function(const source_locationt &l=source_locationt::nil())
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
static instructiont make_incomplete_goto(const exprt &_cond, const source_locationt &l=source_locationt::nil())
Thrown when we can't handle something in an input source file.
const irep_idt & id() const
A side_effect_exprt that returns a non-deterministically chosen value.
const irep_idt & get_identifier() const
symbolt & get_writeable_ref(const irep_idt &name)
Find a symbol in the symbol table for read-write access.
bool has_symbol(const irep_idt &name) const
Check whether a symbol exists in the symbol table.
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
irep_idt base_name
Base (non-scoped) name.
typet type
Type of symbol.
irep_idt mode
Language mode.
static exprt conditional_cast(const exprt &expr, const typet &type)
The type of an expression, extends irept.
Dynamic frame condition checking library loading.
@ WRITE_SET_INSERT_ASSIGNABLE
@ WRITE_SET_HAVOC_GET_ASSIGNABLE_TARGET
@ WRITE_SET_HAVOC_OBJECT_WHOLE
@ CAR_SET_PTR
type of pointers to sets of CAR
@ WRITE_SET_PTR
type of pointers to descriptors of assignable/freeable sets of locations
Enumeration representing the instrumentation mode for loop contracts.
Translate functions that specify assignable and freeable targets declaratively into active functions ...
#define forall_goto_program_instructions(it, program)
#define Forall_goto_program_instructions(it, program)
const std::string & id2string(const irep_idt &d)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
std::string from_expr_using_mode(const namespacet &ns, const irep_idt &mode, const exprt &expr)
Formats an expression using the given namespace, using the given mode to retrieve the language printe...
#define UNREACHABLE
This should be used to mark dead code.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
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.
static void inline_function(goto_modelt &goto_model, const irep_idt &function_id, message_handlert &message_handler)
Inlines the given function, aborts on recursive calls during inlining.
static const exprt make_null_check_expr(const exprt &ptr)
Returns the expression expr == NULL.
static const symbolt & create_new_parameter_symbol(symbol_table_baset &, const irep_idt &function_id, const std::string &base_name, const typet &type)
Creates a new parameter symbol for the given function_id.
static void add_parameter(goto_modelt &, const symbolt &symbol, const irep_idt &function_id)
Adds the given symbol as parameter to the function symbol's code_type.
static symbol_exprt create_symbol(symbol_table_baset &, const typet &type, const irep_idt &function_id, const std::string &base_name, const source_locationt &source_location)
Adds a new symbol named function_id::base_name of type type with given attributes in the symbol table...