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