CBMC
remove_function_pointers.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Remove Indirect Function Calls
4 
5 Author: Daniel Kroening
6 
7 Date: June 2003
8 
9 \*******************************************************************/
10 
13 
14 #ifndef CPROVER_GOTO_PROGRAMS_REMOVE_FUNCTION_POINTERS_H
15 #define CPROVER_GOTO_PROGRAMS_REMOVE_FUNCTION_POINTERS_H
16 
17 #include "goto_program.h"
18 
19 #include <unordered_set>
20 
21 class goto_functionst;
22 class goto_modelt;
23 class message_handlert;
24 class symbol_tablet;
25 
26 // remove indirect function calls
27 // and replace by case-split
29  message_handlert &_message_handler,
30  goto_modelt &goto_model,
31  bool only_remove_const_fps);
32 
43  message_handlert &message_handler,
44  symbol_tablet &symbol_table,
45  goto_programt &goto_program,
46  const irep_idt &function_id,
48  const std::unordered_set<symbol_exprt, irep_hash> &functions);
49 
53  bool return_value_used,
54  const code_typet &call_type,
55  const code_typet &function_type,
56  const namespacet &ns);
57 
61 
65 
66 #endif // CPROVER_GOTO_PROGRAMS_REMOVE_FUNCTION_POINTERS_H
Base type of functions.
Definition: std_types.h:583
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
A collection of goto functions.
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst::iterator targett
Definition: goto_program.h:614
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
The symbol table.
Definition: symbol_table.h:14
Concrete Goto Program.
bool has_function_pointers(const goto_functionst &)
returns true iff any of the given goto functions has function calls via a function pointer
void remove_function_pointer(message_handlert &message_handler, symbol_tablet &symbol_table, goto_programt &goto_program, const irep_idt &function_id, goto_programt::targett target, const std::unordered_set< symbol_exprt, irep_hash > &functions)
Replace a call to a dynamic function at location target in the given goto-program by a case-split ove...
bool function_is_type_compatible(bool return_value_used, const code_typet &call_type, const code_typet &function_type, const namespacet &ns)
Returns true iff call_type can be converted to produce a function call of the same type as function_t...
void remove_function_pointers(message_handlert &_message_handler, goto_modelt &goto_model, bool only_remove_const_fps)