Go to the documentation of this file.
39 bool _add_safety_assertion,
90 bool return_value_used,
95 const typet &call_type,
96 const typet &function_type);
107 bool _add_safety_assertion,
108 bool only_resolve_const_fps,
110 : log(_message_handler),
112 symbol_table(_symbol_table),
113 add_safety_assertion(_add_safety_assertion),
114 only_resolve_const_fps(only_resolve_const_fps)
123 type_map[f_it->first]=f_it->second.type;
127 const typet &call_type,
128 const typet &function_type)
130 if(
type_eq(call_type, function_type,
ns))
134 if(call_type.
id()==ID_signedbv ||
135 call_type.
id()==ID_unsigned ||
136 call_type.
id()==ID_bool ||
137 call_type.
id()==ID_pointer ||
138 call_type.
id()==ID_c_enum ||
139 call_type.
id()==ID_c_enum_tag)
141 if(function_type.
id()==ID_signedbv ||
142 function_type.
id()==ID_unsigned ||
143 function_type.
id()==ID_bool ||
144 function_type.
id()==ID_pointer ||
145 function_type.
id()==ID_c_enum ||
146 function_type.
id()==ID_c_enum_tag)
159 bool return_value_used,
165 if(!return_value_used)
184 function_parameters.empty())
189 call_parameters.empty())
196 if(call_parameters.size()!=function_parameters.size())
199 for(std::size_t i=0; i<call_parameters.size(); i++)
201 function_parameters[i].type()))
220 for(std::size_t i=0; i<function_parameters.size(); i++)
222 if(i<call_arguments.size())
224 if(!
type_eq(call_arguments[i].type(),
225 function_parameters[i].type(),
ns))
227 call_arguments[i].make_typecast(function_parameters[i].type());
250 const symbolt &function_symbol =
258 function_symbol.
mode,
264 function_call.
lhs()=tmp_symbol_expr;
267 t_assign->make_assignment();
285 if(call_type.has_ellipsis() &&
286 call_type.parameters().empty())
288 call_type.remove_ellipsis();
290 call_type.parameters().push_back(
294 bool found_functions;
296 const exprt &pointer =
function.pointer();
299 const auto does_remove_const = const_removal_check();
300 if(does_remove_const.first)
303 log.
warning() <<
"cast from const to non-const pointer found, "
304 <<
"only worst case function pointer removal will be done."
306 found_functions=
false;
313 found_functions=fpr(pointer, functions);
321 if(functions.size()==1)
355 if(t.first==
"pthread_mutex_cleanup")
359 functions.insert(expr);
380 t_final->make_skip();
387 for(
const auto &fun : functions)
391 t1->make_function_call(code);
405 if(address_of.
type()!=pointer.
type())
409 t4->make_goto(t1,
equal_exprt(pointer, address_of));
417 t->source_location.set_property_class(
"pointer dereference");
418 t->source_location.set_comment(
"invalid function pointer");
431 irep_idt property_class=it->source_location.get_property_class();
433 it->source_location=target->source_location;
434 it->function=target->function;
435 if(!property_class.
empty())
436 it->source_location.set_property_class(property_class);
438 it->source_location.set_comment(
comment);
450 target->code.
swap(code_expression);
455 log.
statistics() <<
"replacing function pointer by " << functions.size()
461 mstream <<
"targets: ";
464 for(
const auto &
function : functions)
469 mstream <<
function.get_identifier();
480 bool did_something=
false;
483 if(target->is_function_call())
498 return did_something;
503 bool did_something=
false;
505 for(goto_functionst::function_mapt::iterator f_it=
524 bool add_safety_assertion,
525 bool only_remove_const_fps)
531 add_safety_assertion,
532 only_remove_const_fps,
542 bool add_safety_assertion,
543 bool only_remove_const_fps)
549 add_safety_assertion,
550 only_remove_const_fps,
558 bool add_safety_assertion,
559 bool only_remove_const_fps)
565 add_safety_assertion,
566 only_remove_const_fps);
Class that provides messages with a built-in verbosity 'level'.
#define Forall_goto_program_instructions(it, program)
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
const irep_idt & get_function() const
bool has_ellipsis() const
void operator()(goto_functionst &goto_functions)
std::unordered_set< irep_idt > address_taken
std::string comment(const rw_set_baset::entryt &entry, bool write)
The type of an expression, extends irept.
std::vector< parametert > parameterst
symbolt & get_fresh_aux_symbol(const typet &type, const std::string &name_prefix, const std::string &basename_prefix, const source_locationt &source_location, const irep_idt &symbol_mode, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with the requested name pattern.
remove_function_pointerst(message_handlert &_message_handler, symbol_tablet &_symbol_table, bool _add_safety_assertion, bool only_resolve_const_fps, const goto_functionst &goto_functions)
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
bool remove_function_pointers(goto_programt &goto_program)
remove_const_function_pointerst::functionst functionst
void compute_location_numbers()
Base class for all expressions.
irep_idt base_name
Base (non-scoped) name.
function_mapt function_map
Expression to hold a symbol (variable)
void fix_argument_types(code_function_callt &function_call)
std::unordered_set< symbol_exprt, irep_hash > functionst
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
targett add_instruction()
Adds an instruction at the end.
bool arg_is_type_compatible(const typet &call_type, const typet &function_type)
typet & type()
Return the type of the expression.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
codet representation of a function call statement.
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
bool type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality at the top level.
symbol_tablet & symbol_table
irep_idt mode
Language mode.
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
const std::string & id2string(const irep_idt &d)
source_locationt source_location
bool remove_function_pointers(message_handlert &_message_handler, symbol_tablet &symbol_table, const goto_functionst &goto_functions, goto_programt &goto_program, bool add_safety_assertion, bool only_remove_const_fps)
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
pointer_typet pointer_type(const typet &subtype)
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
const irep_idt & id() const
const code_function_callt & to_code_function_call(const codet &code)
exprt::operandst argumentst
The Boolean constant false.
const parameterst & parameters() const
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
A collection of goto functions.
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
message_handlert & get_message_handler()
void remove_function_pointer(goto_programt &goto_program, goto_programt::targett target, const functionst &functions)
Replace a call to a dynamic function at location target in the given goto-program by a case-split ove...
goto_functionst goto_functions
GOTO functions.
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
void compute_address_taken_functions(const exprt &src, std::unordered_set< irep_idt > &address_taken)
get all functions whose address is taken
void conditional_output(mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
Generate output to message_stream using output_generator if the configured verbosity is at least as h...
bool only_resolve_const_fps
A generic container class for the GOTO intermediate representation of one function.
bool add_safety_assertion
const typet & return_type() const
#define forall_goto_functions(it, functions)
#define forall_expr(it, expr)
Operator to return the address of an object.
source_locationt & add_source_location()
bool is_type_compatible(bool return_value_used, const code_typet &call_type, const code_typet &function_type)
void make_typecast(const typet &_type)
Create a typecast_exprt to the given type.
Semantic type conversion.
void fix_return_type(code_function_callt &function_call, goto_programt &dest)
A codet representing an assignment in the program.
The Boolean constant true.
mstreamt & warning() const
const source_locationt & source_location() const
symbol_tablet symbol_table
Symbol table.
std::map< irep_idt, code_typet > type_mapt
instructionst::iterator targett
codet representation of an expression statement.
mstreamt & statistics() const
#define CHECK_RETURN(CONDITION)