39 bool _add_safety_assertion,
70 bool return_value_used,
75 const typet &call_type,
76 const typet &function_type);
96 bool _add_safety_assertion,
bool only_resolve_const_fps,
100 symbol_table(_symbol_table),
101 add_safety_assertion(_add_safety_assertion),
102 only_resolve_const_fps(only_resolve_const_fps)
109 type_map[f_it->first]=f_it->second.type;
113 const typet &call_type,
114 const typet &function_type)
116 if(
type_eq(call_type, function_type,
ns))
120 if(call_type.
id()==ID_signedbv ||
121 call_type.
id()==ID_unsigned ||
122 call_type.
id()==ID_bool ||
123 call_type.
id()==ID_pointer ||
124 call_type.
id()==ID_c_enum ||
125 call_type.
id()==ID_c_enum_tag)
127 if(function_type.
id()==ID_signedbv ||
128 function_type.
id()==ID_unsigned ||
129 function_type.
id()==ID_bool ||
130 function_type.
id()==ID_pointer ||
131 function_type.
id()==ID_c_enum ||
132 function_type.
id()==ID_c_enum_tag)
145 bool return_value_used,
151 if(!return_value_used)
170 function_parameters.empty())
175 call_parameters.empty())
182 if(call_parameters.size()!=function_parameters.size())
185 for(
unsigned i=0; i<call_parameters.size(); i++)
187 function_parameters[i].type()))
206 for(
unsigned i=0; i<function_parameters.size(); i++)
208 if(i<call_arguments.size())
210 if(!
type_eq(call_arguments[i].type(),
211 function_parameters[i].type(),
ns))
213 call_arguments[i].make_typecast(function_parameters[i].type());
239 "remove_function_pointers",
246 tmp_symbol_expr.
type()=tmp_symbol.
type;
247 tmp_symbol_expr.set_identifier(tmp_symbol.
name);
250 function_call.
lhs()=tmp_symbol_expr;
253 t_assign->make_assignment();
280 assert(
function.
id()==ID_dereference);
281 assert(
function.operands().size()==1);
283 bool found_functions;
285 const exprt &pointer=
function.
op0();
288 if(const_removal_check())
290 warning() <<
"Cast from const to non-const pointer found, only worst case" 291 <<
" function pointer removal will be done." <<
eom;
292 found_functions=
false;
299 found_functions=fpr(pointer, functions);
307 if(functions.size()==1)
341 if(t.first==
"pthread_mutex_cleanup")
345 expr.
type()=t.second;
347 functions.insert(expr);
355 t_final->make_skip();
362 for(
const auto &fun : functions)
366 t1->make_function_call(code);
380 if(address_of.
type()!=pointer.
type())
384 t4->make_goto(t1,
equal_exprt(pointer, address_of));
392 t->source_location.set_property_class(
"pointer dereference");
393 t->source_location.set_comment(
"invalid function pointer");
406 irep_idt property_class=it->source_location.get_property_class();
408 it->source_location=target->source_location;
409 it->function=target->function;
410 if(!property_class.
empty())
411 it->source_location.set_property_class(property_class);
413 it->source_location.set_comment(
comment);
426 target->code.
swap(code_expression);
431 statistics() <<
"replacing function pointer by " 432 << functions.size() <<
" possible targets" <<
eom;
438 bool did_something=
false;
441 if(target->is_function_call())
459 return did_something;
464 bool did_something=
false;
466 for(goto_functionst::function_mapt::iterator f_it=
485 bool add_safety_assertion,
486 bool only_remove_const_fps)
492 add_safety_assertion,
493 only_remove_const_fps,
503 bool add_safety_assertion,
504 bool only_remove_const_fps)
510 add_safety_assertion,
511 only_remove_const_fps,
519 bool add_safety_assertion,
520 bool only_remove_const_fps)
526 add_safety_assertion,
527 only_remove_const_fps);
bool type_eq(const typet &type1, const typet &type2, const namespacet &ns)
The type of an expression.
irep_idt name
The unique identifier.
const typet & follow(const typet &src) const
void update()
Update all indices.
targett add_instruction()
Adds an instruction at the end.
bool is_type_compatible(bool return_value_used, const code_typet &call_type, const code_typet &function_type)
pointer_typet pointer_type(const typet &subtype)
void compute_address_taken_functions(const exprt &src, std::set< irep_idt > &address_taken)
get all functions whose address is taken
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_tablet &symbol_table)
Installs a fresh-named symbol with the requested name pattern.
const symbol_tablet & get_symbol_table() const
Remove Indirect Function Calls.
std::string comment(const rw_set_baset::entryt &entry, bool write)
bool has_ellipsis() const
void fix_return_type(code_function_callt &function_call, goto_programt &dest)
#define forall_expr(it, expr)
Fresh auxiliary symbol creation.
std::vector< parametert > parameterst
exprt::operandst argumentst
symbol_tablet symbol_table
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
#define CHECK_RETURN(CONDITION)
static mstreamt & eom(mstreamt &m)
std::set< irep_idt > address_taken
bool arg_is_type_compatible(const typet &call_type, const typet &function_type)
symbol_tablet & symbol_table
std::unordered_set< exprt, irep_hash > functionst
bool only_resolve_const_fps
void operator()(goto_functionst &goto_functions)
const irep_idt & id() const
The boolean constant true.
void compute_location_numbers()
source_locationt source_location
API to expression classes.
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)
std::map< irep_idt, code_typet > type_mapt
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)
Operator to return the address of an object.
function_mapt function_map
The boolean constant false.
void fix_argument_types(code_function_callt &function_call)
bool remove_function_pointers(goto_programt &goto_program)
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
typet type
Type of symbol.
void remove_skip(goto_programt &goto_program)
remove unnecessary skip statements
message_handlert & get_message_handler()
bool add_safety_assertion
Base class for all expressions.
const parameterst & parameters() const
const source_locationt & source_location() const
void remove_function_pointer(goto_programt &goto_program, goto_programt::targett target)
const exprt & expression() const
const code_typet & to_code_type(const typet &type)
Cast a generic typet to a code_typet.
void set_identifier(const irep_idt &identifier)
source_locationt & add_source_location()
#define Forall_goto_program_instructions(it, program)
void destructive_insert(const_targett target, goto_program_templatet< codeT, guardT > &p)
Inserts the given program at the given location.
Expression to hold a symbol (variable)
void destructive_append(goto_program_templatet< codeT, guardT > &p)
Appends the given program, which is destroyed.
#define forall_goto_functions(it, functions)
void compute_address_taken_in_symbols(std::set< irep_idt > &address_taken)
void make_typecast(const typet &_type)
goto_functionst goto_functions
const typet & return_type() const
const code_function_callt & to_code_function_call(const codet &code)
instructionst::iterator targett