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 #include "goto_model.h"
18 #include <util/message.h>
19 
20 // remove indirect function calls
21 // and replace by case-split
23  message_handlert &_message_handler,
24  goto_modelt &goto_model,
25  bool add_safety_assertion,
26  bool only_remove_const_fps=false);
27 
29  message_handlert &_message_handler,
30  symbol_tablet &symbol_table,
31  goto_functionst &goto_functions,
32  bool add_safety_assertion,
33  bool only_remove_const_fps=false);
34 
36  message_handlert &_message_handler,
37  symbol_tablet &symbol_table,
38  const goto_functionst &goto_functions,
39  goto_programt &goto_program,
40  bool add_safety_assertion,
41  bool only_remove_const_fps=false);
42 
43 #endif // CPROVER_GOTO_PROGRAMS_REMOVE_FUNCTION_POINTERS_H
Symbol Table + CFG.
void remove_function_pointers(message_handlert &_message_handler, goto_modelt &goto_model, bool add_safety_assertion, bool only_remove_const_fps=false)
The symbol table.
Definition: symbol_table.h:52
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24