cprover
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 class goto_functionst;
18 class goto_programt;
19 class goto_modelt;
20 class message_handlert;
21 class symbol_tablet;
22 
23 // remove indirect function calls
24 // and replace by case-split
26  message_handlert &_message_handler,
27  goto_modelt &goto_model,
28  bool add_safety_assertion,
29  bool only_remove_const_fps=false);
30 
32  message_handlert &_message_handler,
33  symbol_tablet &symbol_table,
34  goto_functionst &goto_functions,
35  bool add_safety_assertion,
36  bool only_remove_const_fps=false);
37 
39  message_handlert &_message_handler,
40  symbol_tablet &symbol_table,
41  const goto_functionst &goto_functions,
42  goto_programt &goto_program,
43  bool add_safety_assertion,
44  bool only_remove_const_fps=false);
45 
46 #endif // CPROVER_GOTO_PROGRAMS_REMOVE_FUNCTION_POINTERS_H
symbol_tablet
The symbol table.
Definition: symbol_table.h:19
remove_function_pointers
void remove_function_pointers(message_handlert &_message_handler, goto_modelt &goto_model, bool add_safety_assertion, bool only_remove_const_fps=false)
Definition: remove_function_pointers.cpp:556
goto_modelt
Definition: goto_model.h:24
message_handlert
Definition: message.h:24
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:22
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72