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/base_type.h>
17 #include <util/c_types.h>
18 #include <util/fresh_symbol.h>
19 #include <util/invariant.h>
20 #include <util/message.h>
22 #include <util/replace_expr.h>
23 #include <util/source_location.h>
24 #include <util/std_expr.h>
25 #include <util/type_eq.h>
26 
28 
29 #include "remove_skip.h"
32 
34 {
35 public:
37  message_handlert &_message_handler,
38  symbol_tablet &_symbol_table,
39  bool _add_safety_assertion,
41  const goto_functionst &goto_functions);
42 
43  void operator()(goto_functionst &goto_functions);
44 
45  bool remove_function_pointers(goto_programt &goto_program);
46 
47  // a set of function symbols
49 
57  goto_programt &goto_program,
59  const functionst &functions);
60 
61 protected:
63  const namespacet ns;
66 
67  // We can optionally halt the FP removal if we aren't able to use
68  // remove_const_function_pointerst to successfully narrow to a small
69  // subset of possible functions and just leave the function pointer
70  // as it is.
71  // This can be activated in goto-instrument using
72  // --remove-const-function-pointers instead of --remove-function-pointers
74 
81  goto_programt &goto_program,
82  goto_programt::targett target);
83 
84  std::unordered_set<irep_idt> address_taken;
85 
86  typedef std::map<irep_idt, code_typet> type_mapt;
88 
89  bool is_type_compatible(
90  bool return_value_used,
91  const code_typet &call_type,
92  const code_typet &function_type);
93 
95  const typet &call_type,
96  const typet &function_type);
97 
98  void fix_argument_types(code_function_callt &function_call);
99  void fix_return_type(
100  code_function_callt &function_call,
101  goto_programt &dest);
102 };
103 
105  message_handlert &_message_handler,
106  symbol_tablet &_symbol_table,
107  bool _add_safety_assertion,
108  bool only_resolve_const_fps,
109  const goto_functionst &goto_functions)
110  : log(_message_handler),
111  ns(_symbol_table),
112  symbol_table(_symbol_table),
113  add_safety_assertion(_add_safety_assertion),
114  only_resolve_const_fps(only_resolve_const_fps)
115 {
116  for(const auto &s : symbol_table.symbols)
118 
120 
121  // build type map
122  forall_goto_functions(f_it, goto_functions)
123  type_map[f_it->first]=f_it->second.type;
124 }
125 
127  const typet &call_type,
128  const typet &function_type)
129 {
130  if(type_eq(call_type, function_type, ns))
131  return true;
132 
133  // any integer-vs-enum-vs-pointer is ok
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)
140  {
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)
147  return true;
148 
149  return false;
150  }
151 
152  return pointer_offset_bits(call_type, ns) ==
153  pointer_offset_bits(function_type, ns);
154 
155  return false;
156 }
157 
159  bool return_value_used,
160  const code_typet &call_type,
161  const code_typet &function_type)
162 {
163  // we are willing to ignore anything that's returned
164  // if we call with 'void'
165  if(!return_value_used)
166  {
167  }
168  else if(type_eq(call_type.return_type(), empty_typet(), ns))
169  {
170  // ok
171  }
172  else
173  {
174  if(!arg_is_type_compatible(call_type.return_type(),
175  function_type.return_type()))
176  return false;
177  }
178 
179  // let's look at the parameters
180  const code_typet::parameterst &call_parameters=call_type.parameters();
181  const code_typet::parameterst &function_parameters=function_type.parameters();
182 
183  if(function_type.has_ellipsis() &&
184  function_parameters.empty())
185  {
186  // always ok
187  }
188  else if(call_type.has_ellipsis() &&
189  call_parameters.empty())
190  {
191  // always ok
192  }
193  else
194  {
195  // we are quite strict here, could be much more generous
196  if(call_parameters.size()!=function_parameters.size())
197  return false;
198 
199  for(std::size_t i=0; i<call_parameters.size(); i++)
200  if(!arg_is_type_compatible(call_parameters[i].type(),
201  function_parameters[i].type()))
202  return false;
203  }
204 
205  return true;
206 }
207 
209  code_function_callt &function_call)
210 {
211  const code_typet &code_type=
212  to_code_type(ns.follow(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(!type_eq(call_arguments[i].type(),
225  function_parameters[i].type(), ns))
226  {
227  call_arguments[i].make_typecast(function_parameters[i].type());
228  }
229  }
230  }
231 }
232 
234  code_function_callt &function_call,
235  goto_programt &dest)
236 {
237  // are we returning anything at all?
238  if(function_call.lhs().is_nil())
239  return;
240 
241  const code_typet &code_type=
242  to_code_type(ns.follow(function_call.function().type()));
243 
244  // type already ok?
245  if(type_eq(
246  function_call.lhs().type(),
247  code_type.return_type(), ns))
248  return;
249 
250  const symbolt &function_symbol =
251  ns.lookup(to_symbol_expr(function_call.function()).get_identifier());
252 
253  symbolt &tmp_symbol = get_fresh_aux_symbol(
254  code_type.return_type(),
255  id2string(function_call.source_location().get_function()),
256  "tmp_return_val_" + id2string(function_symbol.base_name),
257  function_call.source_location(),
258  function_symbol.mode,
259  symbol_table);
260 
261  const symbol_exprt tmp_symbol_expr = tmp_symbol.symbol_expr();
262 
263  exprt old_lhs=function_call.lhs();
264  function_call.lhs()=tmp_symbol_expr;
265 
266  goto_programt::targett t_assign=dest.add_instruction();
267  t_assign->make_assignment();
268  t_assign->code=code_assignt(
269  old_lhs, typecast_exprt(tmp_symbol_expr, old_lhs.type()));
270 }
271 
273  goto_programt &goto_program,
274  goto_programt::targett target)
275 {
276  const code_function_callt &code=
277  to_code_function_call(target->code);
278 
279  const auto &function = to_dereference_expr(code.function());
280 
281  // this better have the right type
282  code_typet call_type=to_code_type(function.type());
283 
284  // refine the type in case the forward declaration was incomplete
285  if(call_type.has_ellipsis() &&
286  call_type.parameters().empty())
287  {
288  call_type.remove_ellipsis();
289  forall_expr(it, code.arguments())
290  call_type.parameters().push_back(
291  code_typet::parametert(it->type()));
292  }
293 
294  bool found_functions;
295 
296  const exprt &pointer = function.pointer();
298  does_remove_constt const_removal_check(goto_program, ns);
299  const auto does_remove_const = const_removal_check();
300  if(does_remove_const.first)
301  {
302  log.warning().source_location = does_remove_const.second;
303  log.warning() << "cast from const to non-const pointer found, "
304  << "only worst case function pointer removal will be done."
305  << messaget::eom;
306  found_functions=false;
307  }
308  else
309  {
312 
313  found_functions=fpr(pointer, functions);
314 
315  // if found_functions is false, functions should be empty
316  // however, it is possible for found_functions to be true and functions
317  // to be empty (this happens if the pointer can only resolve to the null
318  // pointer)
319  CHECK_RETURN(found_functions || functions.empty());
320 
321  if(functions.size()==1)
322  {
323  to_code_function_call(target->code).function()=*functions.cbegin();
324  return;
325  }
326  }
327 
328  if(!found_functions)
329  {
331  {
332  // If this mode is enabled, we only remove function pointers
333  // that we can resolve either to an exact function, or an exact subset
334  // (e.g. a variable index in a constant array).
335  // Since we haven't found functions, we would now resort to
336  // replacing the function pointer with any function with a valid signature
337  // Since we don't want to do that, we abort.
338  return;
339  }
340 
341  bool return_value_used=code.lhs().is_not_nil();
342 
343  // get all type-compatible functions
344  // whose address is ever taken
345  for(const auto &t : type_map)
346  {
347  // address taken?
348  if(address_taken.find(t.first)==address_taken.end())
349  continue;
350 
351  // type-compatible?
352  if(!is_type_compatible(return_value_used, call_type, t.second))
353  continue;
354 
355  if(t.first=="pthread_mutex_cleanup")
356  continue;
357 
358  symbol_exprt expr(t.first, t.second);
359  functions.insert(expr);
360  }
361  }
362 
363  remove_function_pointer(goto_program, target, functions);
364 }
365 
367  goto_programt &goto_program,
368  goto_programt::targett target,
369  const functionst &functions)
370 {
371  const code_function_callt &code = to_code_function_call(target->code);
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_instruction();
380  t_final->make_skip();
381 
382  // build the calls and gotos
383 
384  goto_programt new_code_calls;
385  goto_programt new_code_gotos;
386 
387  for(const auto &fun : functions)
388  {
389  // call function
390  goto_programt::targett t1=new_code_calls.add_instruction();
391  t1->make_function_call(code);
392  to_code_function_call(t1->code).function()=fun;
393 
394  // the signature of the function might not match precisely
396 
397  fix_return_type(to_code_function_call(t1->code), new_code_calls);
398  // goto final
399  goto_programt::targett t3=new_code_calls.add_instruction();
400  t3->make_goto(t_final, true_exprt());
401 
402  // goto to call
403  address_of_exprt address_of(fun, pointer_type(fun.type()));
404 
405  if(address_of.type()!=pointer.type())
406  address_of.make_typecast(pointer.type());
407 
408  goto_programt::targett t4=new_code_gotos.add_instruction();
409  t4->make_goto(t1, equal_exprt(pointer, address_of));
410  }
411 
412  // fall-through
414  {
415  goto_programt::targett t=new_code_gotos.add_instruction();
416  t->make_assertion(false_exprt());
417  t->source_location.set_property_class("pointer dereference");
418  t->source_location.set_comment("invalid function pointer");
419  }
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  it->function=target->function;
435  if(!property_class.empty())
436  it->source_location.set_property_class(property_class);
437  if(!comment.empty())
438  it->source_location.set_comment(comment);
439  }
440 
441  goto_programt::targett next_target=target;
442  next_target++;
443 
444  goto_program.destructive_insert(next_target, new_code);
445 
446  // We preserve the original dereferencing to possibly catch
447  // further pointer-related errors.
448  code_expressiont code_expression(function);
449  code_expression.add_source_location()=function.source_location();
450  target->code.swap(code_expression);
451  target->type=OTHER;
452 
453  // report statistics
454  log.statistics().source_location = target->source_location;
455  log.statistics() << "replacing function pointer by " << functions.size()
456  << " possible targets" << messaget::eom;
457 
458  // list the names of functions when verbosity is at debug level
460  log.debug(), [&functions](messaget::mstreamt &mstream) {
461  mstream << "targets: ";
462 
463  bool first = true;
464  for(const auto &function : functions)
465  {
466  if(!first)
467  mstream << ", ";
468 
469  mstream << function.get_identifier();
470  first = false;
471  }
472 
473  mstream << messaget::eom;
474  });
475 }
476 
478  goto_programt &goto_program)
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=
486  to_code_function_call(target->code);
487 
488  if(code.function().id()==ID_dereference)
489  {
490  remove_function_pointer(goto_program, target);
491  did_something=true;
492  }
493  }
494 
495  if(did_something)
496  remove_skip(goto_program);
497 
498  return did_something;
499 }
500 
502 {
503  bool did_something=false;
504 
505  for(goto_functionst::function_mapt::iterator f_it=
506  functions.function_map.begin();
507  f_it!=functions.function_map.end();
508  f_it++)
509  {
510  goto_programt &goto_program=f_it->second.body;
511 
512  if(remove_function_pointers(goto_program))
513  did_something=true;
514  }
515 
516  if(did_something)
517  functions.compute_location_numbers();
518 }
519 
521  symbol_tablet &symbol_table,
522  const goto_functionst &goto_functions,
523  goto_programt &goto_program,
524  bool add_safety_assertion,
525  bool only_remove_const_fps)
526 {
528  rfp(
529  _message_handler,
530  symbol_table,
531  add_safety_assertion,
532  only_remove_const_fps,
533  goto_functions);
534 
535  return rfp.remove_function_pointers(goto_program);
536 }
537 
539  message_handlert &_message_handler,
540  symbol_tablet &symbol_table,
541  goto_functionst &goto_functions,
542  bool add_safety_assertion,
543  bool only_remove_const_fps)
544 {
546  rfp(
547  _message_handler,
548  symbol_table,
549  add_safety_assertion,
550  only_remove_const_fps,
551  goto_functions);
552 
553  rfp(goto_functions);
554 }
555 
557  goto_modelt &goto_model,
558  bool add_safety_assertion,
559  bool only_remove_const_fps)
560 {
562  _message_handler,
563  goto_model.symbol_table,
564  goto_model.goto_functions,
565  add_safety_assertion,
566  only_remove_const_fps);
567 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:144
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:809
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
pointer_offset_size.h
source_locationt::get_function
const irep_idt & get_function() const
Definition: source_location.h:57
code_typet::has_ellipsis
bool has_ellipsis() const
Definition: std_types.h:849
symbol_tablet
The symbol table.
Definition: symbol_table.h:19
remove_function_pointerst::operator()
void operator()(goto_functionst &goto_functions)
Definition: remove_function_pointers.cpp:501
remove_function_pointerst::address_taken
std::unordered_set< irep_idt > address_taken
Definition: remove_function_pointers.cpp:84
comment
std::string comment(const rw_set_baset::entryt &entry, bool write)
Definition: race_check.cpp:107
typet
The type of an expression, extends irept.
Definition: type.h:27
code_typet::parameterst
std::vector< parametert > parameterst
Definition: std_types.h:754
fresh_symbol.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, symbol_table_baset &symbol_table)
Installs a fresh-named symbol with the requested name pattern.
Definition: fresh_symbol.cpp:30
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:104
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:86
remove_function_pointerst::remove_function_pointers
bool remove_function_pointers(goto_programt &goto_program)
Definition: remove_function_pointers.cpp:477
remove_function_pointerst::functionst
remove_const_function_pointerst::functionst functionst
Definition: remove_function_pointers.cpp:48
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:24
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
invariant.h
messaget::eom
static eomt eom
Definition: message.h:284
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:143
equal_exprt
Equality.
Definition: std_expr.h:1484
remove_function_pointerst::fix_argument_types
void fix_argument_types(code_function_callt &function_call)
Definition: remove_function_pointers.cpp:208
code_function_callt::lhs
exprt & lhs()
Definition: std_code.h:1089
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:93
goto_programt::add_instruction
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:541
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:126
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
namespacet::lookup
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:166
code_function_callt
codet representation of a function call statement.
Definition: std_code.h:1036
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:173
remove_function_pointerst::type_map
type_mapt type_map
Definition: remove_function_pointers.cpp:87
type_eq.h
to_code_type
const code_typet & to_code_type(const typet &type)
Cast a typet to a code_typet.
Definition: std_types.h:982
type_eq
bool type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality at the top level.
Definition: type_eq.cpp:31
remove_function_pointerst::symbol_table
symbol_tablet & symbol_table
Definition: remove_function_pointers.cpp:64
symbolt::mode
irep_idt mode
Language mode.
Definition: symbol.h:49
empty_typet
The empty type.
Definition: std_types.h:48
base_type.h
goto_programt::destructive_insert
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
Definition: goto_program.h:532
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
remove_function_pointerst::log
messaget log
Definition: remove_function_pointers.cpp:62
messaget::mstreamt::source_location
source_locationt source_location
Definition: message.h:236
remove_function_pointers
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)
Definition: remove_function_pointers.cpp:520
dereference_exprt::pointer
exprt & pointer()
Definition: std_expr.h:3380
pointer_offset_bits
optionalt< mp_integer > pointer_offset_bits(const typet &type, const namespacet &ns)
Definition: pointer_offset_size.cpp:101
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
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:303
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
code_typet
Base type of functions.
Definition: std_types.h:751
OTHER
Definition: goto_program.h:37
irept::is_nil
bool is_nil() const
Definition: irep.h:172
irept::id
const irep_idt & id() const
Definition: irep.h:259
message_handlert
Definition: message.h:24
to_code_function_call
const code_function_callt & to_code_function_call(const codet &code)
Definition: std_code.h:1173
code_function_callt::argumentst
exprt::operandst argumentst
Definition: std_code.h:1055
dstringt::empty
bool empty() const
Definition: dstring.h:75
false_exprt
The Boolean constant false.
Definition: std_expr.h:4452
code_typet::parameters
const parameterst & parameters() const
Definition: std_types.h:893
code_function_callt::arguments
argumentst & arguments()
Definition: std_code.h:1109
remove_const_function_pointerst
Definition: remove_const_function_pointers.h:32
does_remove_constt
Definition: does_remove_const.h:21
goto_programt::destructive_append
void destructive_append(goto_programt &p)
Appends the given program p to *this. p is destroyed.
Definition: goto_program.h:524
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:22
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: std_expr.h:3397
messaget::get_message_handler
message_handlert & get_message_handler()
Definition: message.h:174
remove_function_pointerst::remove_function_pointer
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...
Definition: remove_function_pointers.cpp:366
remove_const_function_pointers.h
does_remove_const.h
goto_modelt::goto_functions
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
namespace_baset::follow
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition: namespace.cpp:62
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:27
symbol_table_baset::symbols
const symbolst & symbols
Definition: symbol_table_base.h:27
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:132
remove_function_pointerst::only_resolve_const_fps
bool only_resolve_const_fps
Definition: remove_function_pointers.cpp:73
code_typet::parametert
Definition: std_types.h:788
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
remove_function_pointerst::add_safety_assertion
bool add_safety_assertion
Definition: remove_function_pointers.cpp:65
code_typet::return_type
const typet & return_type() const
Definition: std_types.h:883
forall_goto_functions
#define forall_goto_functions(it, functions)
Definition: goto_functions.h:149
messaget::mstreamt
Definition: message.h:212
replace_expr.h
compute_called_functions.h
messaget::debug
mstreamt & debug() const
Definition: message.h:416
forall_expr
#define forall_expr(it, expr)
Definition: expr.h:31
remove_function_pointerst::ns
const namespacet ns
Definition: remove_function_pointers.cpp:63
address_of_exprt
Operator to return the address of an object.
Definition: std_expr.h:3255
exprt::add_source_location
source_locationt & add_source_location()
Definition: expr.h:233
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:158
exprt::make_typecast
void make_typecast(const typet &_type)
Create a typecast_exprt to the given type.
Definition: expr.cpp:74
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2277
remove_function_pointerst::fix_return_type
void fix_return_type(code_function_callt &function_call, goto_programt &dest)
Definition: remove_function_pointers.cpp:233
remove_skip.h
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:256
message.h
true_exprt
The Boolean constant true.
Definition: std_expr.h:4443
messaget::warning
mstreamt & warning() const
Definition: message.h:391
std_expr.h
remove_function_pointers.h
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:228
goto_modelt::symbol_table
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
c_types.h
remove_function_pointerst::type_mapt
std::map< irep_idt, code_typet > type_mapt
Definition: remove_function_pointers.cpp:86
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:414
code_function_callt::function
exprt & function()
Definition: std_code.h:1099
remove_function_pointerst
Definition: remove_function_pointers.cpp:33
code_expressiont
codet representation of an expression statement.
Definition: std_code.h:1504
messaget::statistics
mstreamt & statistics() const
Definition: message.h:406
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:470