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
25
void
remove_function_pointers
(
26
message_handlert
&_message_handler,
27
goto_modelt
&goto_model,
28
bool
add_safety_assertion,
29
bool
only_remove_const_fps=
false
);
30
31
void
remove_function_pointers
(
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
38
bool
remove_function_pointers
(
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
goto_modelt
Definition:
goto_model.h:24
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:532
symbol_tablet
The symbol table.
Definition:
symbol_table.h:19
message_handlert
Definition:
message.h:25
goto_functionst
Definition:
goto_functions.h:21
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition:
goto_program.h:70
goto_program
goto_programt & goto_program
Definition:
cover.cpp:63
goto-programs
remove_function_pointers.h
Generated by
1.8.14