cprover
remove_function_pointers.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Program Transformation
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
13 
14 #include <util/c_types.h>
15 #include <util/fresh_symbol.h>
16 #include <util/invariant.h>
17 #include <util/message.h>
18 #include <util/pointer_expr.h>
20 #include <util/replace_expr.h>
21 #include <util/source_location.h>
22 #include <util/std_expr.h>
23 
25 
26 #include "remove_skip.h"
29 
31 {
32 public:
34  message_handlert &_message_handler,
35  symbol_tablet &_symbol_table,
36  bool _add_safety_assertion,
38  const goto_functionst &goto_functions);
39 
40  void operator()(goto_functionst &goto_functions);
41 
43  goto_programt &goto_program,
44  const irep_idt &function_id);
45 
46  // a set of function symbols
48 
57  goto_programt &goto_program,
58  const irep_idt &function_id,
60  const functionst &functions);
61 
62 protected:
64  const namespacet ns;
67 
68  // We can optionally halt the FP removal if we aren't able to use
69  // remove_const_function_pointerst to successfully narrow to a small
70  // subset of possible functions and just leave the function pointer
71  // as it is.
72  // This can be activated in goto-instrument using
73  // --remove-const-function-pointers instead of --remove-function-pointers
75 
83  goto_programt &goto_program,
84  const irep_idt &function_id,
85  goto_programt::targett target);
86 
87  std::unordered_set<irep_idt> address_taken;
88 
89  typedef std::map<irep_idt, code_typet> type_mapt;
91 
92  bool is_type_compatible(
93  bool return_value_used,
94  const code_typet &call_type,
95  const code_typet &function_type);
96 
98  const typet &call_type,
99  const typet &function_type);
100 
101  void fix_argument_types(code_function_callt &function_call);
102  void fix_return_type(
103  const irep_idt &in_function_id,
104  code_function_callt &function_call,
105  goto_programt &dest);
106 };
107 
109  message_handlert &_message_handler,
110  symbol_tablet &_symbol_table,
111  bool _add_safety_assertion,
112  bool only_resolve_const_fps,
113  const goto_functionst &goto_functions)
114  : log(_message_handler),
115  ns(_symbol_table),
116  symbol_table(_symbol_table),
117  add_safety_assertion(_add_safety_assertion),
118  only_resolve_const_fps(only_resolve_const_fps)
119 {
120  for(const auto &s : symbol_table.symbols)
122 
124 
125  // build type map
126  for(const auto &gf_entry : goto_functions.function_map)
127  {
128  type_map.emplace(
129  gf_entry.first, to_code_type(ns.lookup(gf_entry.first).type));
130  }
131 }
132 
134  const typet &call_type,
135  const typet &function_type)
136 {
137  if(call_type == function_type)
138  return true;
139 
140  // any integer-vs-enum-vs-pointer is ok
141  if(
142  call_type.id() == ID_signedbv || call_type.id() == ID_unsigned ||
143  call_type.id() == ID_bool || call_type.id() == ID_c_bool ||
144  call_type.id() == ID_c_enum_tag || call_type.id() == ID_c_enum ||
145  call_type.id() == ID_pointer)
146  {
147  return function_type.id() == ID_signedbv ||
148  function_type.id() == ID_unsigned || function_type.id() == ID_bool ||
149  function_type.id() == ID_c_bool ||
150  function_type.id() == ID_pointer ||
151  function_type.id() == ID_c_enum ||
152  function_type.id() == ID_c_enum_tag;
153  }
154 
155  return pointer_offset_bits(call_type, ns) ==
156  pointer_offset_bits(function_type, ns);
157 }
158 
160  bool return_value_used,
161  const code_typet &call_type,
162  const code_typet &function_type)
163 {
164  // we are willing to ignore anything that's returned
165  // if we call with 'void'
166  if(!return_value_used)
167  {
168  }
169  else if(call_type.return_type() == empty_typet())
170  {
171  // ok
172  }
173  else
174  {
175  if(!arg_is_type_compatible(call_type.return_type(),
176  function_type.return_type()))
177  return false;
178  }
179 
180  // let's look at the parameters
181  const code_typet::parameterst &call_parameters=call_type.parameters();
182  const code_typet::parameterst &function_parameters=function_type.parameters();
183 
184  if(function_type.has_ellipsis() &&
185  function_parameters.empty())
186  {
187  // always ok
188  }
189  else if(call_type.has_ellipsis() &&
190  call_parameters.empty())
191  {
192  // always ok
193  }
194  else
195  {
196  // we are quite strict here, could be much more generous
197  if(call_parameters.size()!=function_parameters.size())
198  return false;
199 
200  for(std::size_t i=0; i<call_parameters.size(); i++)
201  if(!arg_is_type_compatible(call_parameters[i].type(),
202  function_parameters[i].type()))
203  return false;
204  }
205 
206  return true;
207 }
208 
210  code_function_callt &function_call)
211 {
212  const code_typet &code_type = to_code_type(function_call.function().type());
213 
214  const code_typet::parameterst &function_parameters=
215  code_type.parameters();
216 
217  code_function_callt::argumentst &call_arguments=
218  function_call.arguments();
219 
220  for(std::size_t i=0; i<function_parameters.size(); i++)
221  {
222  if(i<call_arguments.size())
223  {
224  if(call_arguments[i].type() != function_parameters[i].type())
225  {
226  call_arguments[i] =
227  typecast_exprt(call_arguments[i], function_parameters[i].type());
228  }
229  }
230  }
231 }
232 
234  const irep_idt &in_function_id,
235  code_function_callt &function_call,
236  goto_programt &dest)
237 {
238  // are we returning anything at all?
239  if(function_call.lhs().is_nil())
240  return;
241 
242  const code_typet &code_type = to_code_type(function_call.function().type());
243 
244  // type already ok?
245  if(function_call.lhs().type() == code_type.return_type())
246  return;
247 
248  const symbolt &function_symbol =
249  ns.lookup(to_symbol_expr(function_call.function()).get_identifier());
250 
251  symbolt &tmp_symbol = get_fresh_aux_symbol(
252  code_type.return_type(),
253  id2string(in_function_id),
254  "tmp_return_val_" + id2string(function_symbol.base_name),
255  function_call.source_location(),
256  function_symbol.mode,
257  symbol_table);
258 
259  const symbol_exprt tmp_symbol_expr = tmp_symbol.symbol_expr();
260 
261  exprt old_lhs=function_call.lhs();
262  function_call.lhs()=tmp_symbol_expr;
263 
265  code_assignt(old_lhs, typecast_exprt(tmp_symbol_expr, old_lhs.type()))));
266 }
267 
269  goto_programt &goto_program,
270  const irep_idt &function_id,
271  goto_programt::targett target)
272 {
273  const code_function_callt &code = target->get_function_call();
274 
275  const auto &function = to_dereference_expr(code.function());
276 
277  // this better have the right type
278  code_typet call_type=to_code_type(function.type());
279 
280  // refine the type in case the forward declaration was incomplete
281  if(call_type.has_ellipsis() &&
282  call_type.parameters().empty())
283  {
284  call_type.remove_ellipsis();
285  for(const auto &argument : code.arguments())
286  {
287  call_type.parameters().push_back(code_typet::parametert(argument.type()));
288  }
289  }
290 
291  bool found_functions;
292 
293  const exprt &pointer = function.pointer();
295  does_remove_constt const_removal_check(goto_program, ns);
296  const auto does_remove_const = const_removal_check();
297  if(does_remove_const.first)
298  {
299  log.warning().source_location = does_remove_const.second;
300  log.warning() << "cast from const to non-const pointer found, "
301  << "only worst case function pointer removal will be done."
302  << messaget::eom;
303  found_functions=false;
304  }
305  else
306  {
309 
310  found_functions=fpr(pointer, functions);
311 
312  // if found_functions is false, functions should be empty
313  // however, it is possible for found_functions to be true and functions
314  // to be empty (this happens if the pointer can only resolve to the null
315  // pointer)
316  CHECK_RETURN(found_functions || functions.empty());
317 
318  if(functions.size()==1)
319  {
320  auto call = target->get_function_call();
321  call.function() = *functions.cbegin();
322  target->set_function_call(call);
323  return;
324  }
325  }
326 
327  if(!found_functions)
328  {
330  {
331  // If this mode is enabled, we only remove function pointers
332  // that we can resolve either to an exact function, or an exact subset
333  // (e.g. a variable index in a constant array).
334  // Since we haven't found functions, we would now resort to
335  // replacing the function pointer with any function with a valid signature
336  // Since we don't want to do that, we abort.
337  return;
338  }
339 
340  bool return_value_used=code.lhs().is_not_nil();
341 
342  // get all type-compatible functions
343  // whose address is ever taken
344  for(const auto &t : type_map)
345  {
346  // address taken?
347  if(address_taken.find(t.first)==address_taken.end())
348  continue;
349 
350  // type-compatible?
351  if(!is_type_compatible(return_value_used, call_type, t.second))
352  continue;
353 
354  if(t.first=="pthread_mutex_cleanup")
355  continue;
356 
357  symbol_exprt expr(t.first, t.second);
358  functions.insert(expr);
359  }
360  }
361 
362  remove_function_pointer(goto_program, function_id, target, functions);
363 }
364 
366  goto_programt &goto_program,
367  const irep_idt &function_id,
368  goto_programt::targett target,
369  const functionst &functions)
370 {
371  const code_function_callt &code = target->get_function_call();
372 
373  const exprt &function = code.function();
374  const exprt &pointer = to_dereference_expr(function).pointer();
375 
376  // the final target is a skip
377  goto_programt final_skip;
378 
379  goto_programt::targett t_final = final_skip.add(goto_programt::make_skip());
380 
381  // build the calls and gotos
382 
383  goto_programt new_code_calls;
384  goto_programt new_code_gotos;
385 
386  for(const auto &fun : functions)
387  {
388  // call function
389  auto new_call = code;
390  new_call.function() = fun;
391 
392  // the signature of the function might not match precisely
393  fix_argument_types(new_call);
394 
395  goto_programt tmp;
396  fix_return_type(function_id, new_call, tmp);
397 
398  auto call = new_code_calls.add(goto_programt::make_function_call(new_call));
399  new_code_calls.destructive_append(tmp);
400 
401  // goto final
402  new_code_calls.add(goto_programt::make_goto(t_final, true_exprt()));
403 
404  // goto to call
405  const address_of_exprt address_of(fun, pointer_type(fun.type()));
406 
407  const auto casted_address =
408  typecast_exprt::conditional_cast(address_of, pointer.type());
409 
410  new_code_gotos.add(
411  goto_programt::make_goto(call, equal_exprt(pointer, casted_address)));
412  }
413 
414  // fall-through
416  {
418  new_code_gotos.add(goto_programt::make_assertion(false_exprt()));
419  t->source_location.set_property_class("pointer dereference");
420  t->source_location.set_comment("invalid function pointer");
421  }
423 
424  goto_programt new_code;
425 
426  // patch them all together
427  new_code.destructive_append(new_code_gotos);
428  new_code.destructive_append(new_code_calls);
429  new_code.destructive_append(final_skip);
430 
431  // set locations
432  for(auto &instruction : new_code.instructions)
433  {
434  source_locationt &source_location = instruction.source_location;
435 
436  irep_idt property_class = source_location.get_property_class();
437  irep_idt comment = source_location.get_comment();
438  source_location = target->source_location;
439  if(!property_class.empty())
440  source_location.set_property_class(property_class);
441  if(!comment.empty())
442  source_location.set_comment(comment);
443  }
444 
445  goto_programt::targett next_target=target;
446  next_target++;
447 
448  goto_program.destructive_insert(next_target, new_code);
449 
450  // We preserve the original dereferencing to possibly catch
451  // further pointer-related errors.
452  code_expressiont code_expression(function);
453  code_expression.add_source_location()=function.source_location();
454  target->code.swap(code_expression);
455  target->type=OTHER;
456 
457  // report statistics
458  log.statistics().source_location = target->source_location;
459  log.statistics() << "replacing function pointer by " << functions.size()
460  << " possible targets" << messaget::eom;
461 
462  // list the names of functions when verbosity is at debug level
464  log.debug(), [&functions](messaget::mstreamt &mstream) {
465  mstream << "targets: ";
466 
467  bool first = true;
468  for(const auto &function : functions)
469  {
470  if(!first)
471  mstream << ", ";
472 
473  mstream << function.get_identifier();
474  first = false;
475  }
476 
477  mstream << messaget::eom;
478  });
479 }
480 
482  goto_programt &goto_program,
483  const irep_idt &function_id)
484 {
485  bool did_something=false;
486 
487  Forall_goto_program_instructions(target, goto_program)
488  if(target->is_function_call())
489  {
490  const code_function_callt &code = target->get_function_call();
491 
492  if(code.function().id()==ID_dereference)
493  {
494  remove_function_pointer(goto_program, function_id, target);
495  did_something=true;
496  }
497  }
498 
499  if(did_something)
500  remove_skip(goto_program);
501 
502  return did_something;
503 }
504 
506 {
507  bool did_something=false;
508 
509  for(goto_functionst::function_mapt::iterator f_it=
510  functions.function_map.begin();
511  f_it!=functions.function_map.end();
512  f_it++)
513  {
514  goto_programt &goto_program=f_it->second.body;
515 
516  if(remove_function_pointers(goto_program, f_it->first))
517  did_something=true;
518  }
519 
520  if(did_something)
521  functions.compute_location_numbers();
522 }
523 
525  message_handlert &_message_handler,
526  symbol_tablet &symbol_table,
527  const goto_functionst &goto_functions,
528  goto_programt &goto_program,
529  const irep_idt &function_id,
530  bool add_safety_assertion,
531  bool only_remove_const_fps)
532 {
534  rfp(
535  _message_handler,
536  symbol_table,
537  add_safety_assertion,
538  only_remove_const_fps,
539  goto_functions);
540 
541  return rfp.remove_function_pointers(goto_program, function_id);
542 }
543 
545  message_handlert &_message_handler,
546  symbol_tablet &symbol_table,
547  goto_functionst &goto_functions,
548  bool add_safety_assertion,
549  bool only_remove_const_fps)
550 {
552  rfp(
553  _message_handler,
554  symbol_table,
555  add_safety_assertion,
556  only_remove_const_fps,
557  goto_functions);
558 
559  rfp(goto_functions);
560 }
561 
563  goto_modelt &goto_model,
564  bool add_safety_assertion,
565  bool only_remove_const_fps)
566 {
568  _message_handler,
569  goto_model.symbol_table,
570  goto_model.goto_functions,
571  add_safety_assertion,
572  only_remove_const_fps);
573 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:1172
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
pointer_offset_size.h
Pointer Logic.
source_locationt::get_comment
const irep_idt & get_comment() const
Definition: source_location.h:71
code_typet::has_ellipsis
bool has_ellipsis() const
Definition: std_types.h:816
typecast_exprt::conditional_cast
static exprt conditional_cast(const exprt &expr, const typet &type)
Definition: std_expr.h:1789
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
source_locationt::get_property_class
const irep_idt & get_property_class() const
Definition: source_location.h:66
remove_function_pointerst::operator()
void operator()(goto_functionst &goto_functions)
Definition: remove_function_pointers.cpp:505
source_locationt::set_comment
void set_comment(const irep_idt &comment)
Definition: source_location.h:141
remove_function_pointerst::address_taken
std::unordered_set< irep_idt > address_taken
Definition: remove_function_pointers.cpp:87
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: pointer_expr.h:312
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
typet
The type of an expression, extends irept.
Definition: type.h:28
code_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:746
fresh_symbol.h
Fresh auxiliary symbol creation.
remove_function_pointerst::remove_function_pointerst
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)
Definition: remove_function_pointers.cpp:108
remove_skip
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:85
remove_function_pointerst::fix_return_type
void fix_return_type(const irep_idt &in_function_id, code_function_callt &function_call, goto_programt &dest)
Definition: remove_function_pointers.cpp:233
invariant.h
remove_function_pointerst::functionst
remove_const_function_pointerst::functionst functionst
Definition: remove_function_pointers.cpp:47
goto_programt::add
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:657
goto_functionst::compute_location_numbers
void compute_location_numbers()
Definition: goto_functions.cpp:18
exprt
Base class for all expressions.
Definition: expr.h:54
goto_modelt
Definition: goto_model.h:26
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
messaget::eom
static eomt eom
Definition: message.h:297
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:27
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:81
equal_exprt
Equality.
Definition: std_expr.h:1140
code_typet::remove_ellipsis
void remove_ellipsis()
Definition: std_types.h:845
remove_function_pointerst::fix_argument_types
void fix_argument_types(code_function_callt &function_call)
Definition: remove_function_pointers.cpp:209
code_function_callt::lhs
exprt & lhs()
Definition: std_code.h:1240
goto_programt::make_assignment
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
Definition: goto_program.h:995
goto_programt::make_goto
static instructiont make_goto(targett _target, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:969
remove_const_function_pointerst::functionst
std::unordered_set< symbol_exprt, irep_hash > functionst
Definition: remove_const_function_pointers.h:35
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
goto_programt::make_function_call
static instructiont make_function_call(const code_function_callt &_code, const source_locationt &l=source_locationt::nil())
Create a function call instruction.
Definition: goto_program.h:1020
remove_function_pointerst::arg_is_type_compatible
bool arg_is_type_compatible(const typet &call_type, const typet &function_type)
Definition: remove_function_pointers.cpp:133
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:140
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1215
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:391
remove_function_pointerst::type_map
type_mapt type_map
Definition: remove_function_pointers.cpp:90
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:949
remove_function_pointerst::remove_function_pointer
void remove_function_pointer(goto_programt &goto_program, const irep_idt &function_id, 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...
Definition: remove_function_pointers.cpp:365
remove_function_pointerst::symbol_table
symbol_tablet & symbol_table
Definition: remove_function_pointers.cpp:65
goto_programt::make_assertion
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:864
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
empty_typet
The empty type.
Definition: std_types.h:46
goto_programt::destructive_insert
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
Definition: goto_program.h:648
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:49
remove_function_pointerst::log
messaget log
Definition: remove_function_pointers.cpp:63
messaget::mstreamt::source_location
source_locationt source_location
Definition: message.h:247
goto_programt::make_skip
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:822
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:110
dereference_exprt::pointer
exprt & pointer()
Definition: pointer_expr.h:269
pointer_offset_bits
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:100
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
pointer_expr.h
API to expression classes for Pointers.
source_location.h
pointer_type
pointer_typet pointer_type(const typet &subtype)
Definition: c_types.cpp:243
irept::swap
void swap(irept &irep)
Definition: irep.h:452
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:190
code_typet
Base type of functions.
Definition: std_types.h:744
OTHER
@ OTHER
Definition: goto_program.h:38
irept::is_nil
bool is_nil() const
Definition: irep.h:387
irept::id
const irep_idt & id() const
Definition: irep.h:407
message_handlert
Definition: message.h:28
code_function_callt::argumentst
exprt::operandst argumentst
Definition: std_code.h:1224
dstringt::empty
bool empty() const
Definition: dstring.h:88
false_exprt
The Boolean constant false.
Definition: std_expr.h:2726
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:860
code_function_callt::arguments
argumentst & arguments()
Definition: std_code.h:1260
remove_const_function_pointerst
Definition: remove_const_function_pointers.h:33
does_remove_constt
Definition: does_remove_const.h:22
goto_programt::destructive_append
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:640
source_locationt
Definition: source_location.h:20
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:556
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
messaget::get_message_handler
message_handlert & get_message_handler()
Definition: message.h:184
remove_const_function_pointers.h
Goto Programs.
does_remove_const.h
Analyses.
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
compute_address_taken_functions
void compute_address_taken_functions(const exprt &src, std::unordered_set< irep_idt > &address_taken)
get all functions whose address is taken
Definition: compute_called_functions.cpp:18
symbolt
Symbol table entry.
Definition: symbol.h:28
symbol_table_baset::symbols
const symbolst & symbols
Read-only field, used to look up symbols given their names.
Definition: symbol_table_base.h:30
messaget::conditional_output
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...
Definition: message.cpp:138
remove_function_pointerst::only_resolve_const_fps
bool only_resolve_const_fps
Definition: remove_function_pointers.cpp:74
code_typet::parametert
Definition: std_types.h:761
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:74
remove_function_pointerst::add_safety_assertion
bool add_safety_assertion
Definition: remove_function_pointers.cpp:66
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:850
messaget::mstreamt
Definition: message.h:224
goto_programt::make_assumption
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:876
replace_expr.h
compute_called_functions.h
Query Called Functions.
messaget::debug
mstreamt & debug() const
Definition: message.h:429
remove_function_pointerst::ns
const namespacet ns
Definition: remove_function_pointers.cpp:64
address_of_exprt
Operator to return the address of an object.
Definition: pointer_expr.h:200
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:239
remove_function_pointerst::is_type_compatible
bool is_type_compatible(bool return_value_used, const code_typet &call_type, const code_typet &function_type)
Definition: remove_function_pointers.cpp:159
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:1781
remove_skip.h
Program Transformation.
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
message.h
true_exprt
The Boolean constant true.
Definition: std_expr.h:2717
remove_function_pointers
bool remove_function_pointers(message_handlert &_message_handler, symbol_tablet &symbol_table, const goto_functionst &goto_functions, goto_programt &goto_program, const irep_idt &function_id, bool add_safety_assertion, bool only_remove_const_fps)
Definition: remove_function_pointers.cpp:524
messaget::warning
mstreamt & warning() const
Definition: message.h:404
comment
static std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:109
std_expr.h
API to expression classes.
remove_function_pointers.h
Remove Indirect Function Calls.
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:234
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:30
c_types.h
get_fresh_aux_symbol
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, const namespacet &ns, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with respect to the given namespace ns with the requested name pattern ...
Definition: fresh_symbol.cpp:32
remove_function_pointerst::type_mapt
std::map< irep_idt, code_typet > type_mapt
Definition: remove_function_pointers.cpp:89
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:550
code_function_callt::function
exprt & function()
Definition: std_code.h:1250
remove_function_pointerst
Definition: remove_function_pointers.cpp:31
code_expressiont
codet representation of an expression statement.
Definition: std_code.h:1842
messaget::statistics
mstreamt & statistics() const
Definition: message.h:419
remove_function_pointerst::remove_function_pointers
bool remove_function_pointers(goto_programt &goto_program, const irep_idt &function_id)
Definition: remove_function_pointers.cpp:481
source_locationt::set_property_class
void set_property_class(const irep_idt &property_class)
Definition: source_location.h:136