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
28 void remove_function_pointers(
29  message_handlert &_message_handler,
30  goto_modelt &goto_model,
31  bool only_remove_const_fps);
32 
42 void remove_function_pointer(
43  message_handlert &message_handler,
44  symbol_tablet &symbol_table,
45  goto_programt &goto_program,
46  const irep_idt &function_id,
47  goto_programt::targett target,
48  const std::unordered_set<symbol_exprt, irep_hash> &functions);
49 
52 bool function_is_type_compatible(
53  bool return_value_used,
54  const code_typet &call_type,
55  const code_typet &function_type,
56  const namespacet &ns);
57 
60 bool has_function_pointers(const goto_functionst &);
61 
64 bool has_function_pointers(const goto_modelt &);
65 
66 #endif // CPROVER_GOTO_PROGRAMS_REMOVE_FUNCTION_POINTERS_H
code_typet
Base type of functions.
Definition: std_types.h:583
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:25
goto_modelt
Definition: goto_model.h:27
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:614
message_handlert
Definition: message.h:27
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
symbol_tablet
The symbol table.
Definition: symbol_table.h:14
goto_program.h
Concrete Goto Program.
has_function_pointers
bool has_function_pointers(const goto_functionst &)
returns true iff any of the given goto functions has function calls via a function pointer
Definition: remove_function_pointers.cpp:553
remove_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...
Definition: remove_function_pointers.cpp:379
function_is_type_compatible
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...
Definition: remove_function_pointers.cpp:129
remove_function_pointers
void remove_function_pointers(message_handlert &_message_handler, goto_modelt &goto_model, bool only_remove_const_fps)
Definition: remove_function_pointers.cpp:526