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 <util/irep.h>
18 
19 class goto_functionst;
20 class goto_programt;
21 class goto_modelt;
22 class message_handlert;
23 class symbol_tablet;
24 
25 // remove indirect function calls
26 // and replace by case-split
28  message_handlert &_message_handler,
29  goto_modelt &goto_model,
30  bool add_safety_assertion,
31  bool only_remove_const_fps=false);
32 
34  message_handlert &_message_handler,
35  symbol_tablet &symbol_table,
36  goto_functionst &goto_functions,
37  bool add_safety_assertion,
38  bool only_remove_const_fps=false);
39 
41  message_handlert &_message_handler,
42  symbol_tablet &symbol_table,
43  const goto_functionst &goto_functions,
44  goto_programt &goto_program,
45  const irep_idt &function_id,
46  bool add_safety_assertion,
47  bool only_remove_const_fps = false);
48 
49 #endif // CPROVER_GOTO_PROGRAMS_REMOVE_FUNCTION_POINTERS_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
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:557
goto_modelt
Definition: goto_model.h:26
message_handlert
Definition: message.h:28
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
irep.h