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
22
void
remove_function_pointers
(
23
message_handlert
&_message_handler,
24
goto_modelt
&goto_model,
25
bool
add_safety_assertion,
26
bool
only_remove_const_fps=
false
);
27
28
void
remove_function_pointers
(
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
35
bool
remove_function_pointers
(
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
message.h
goto_modelt
Definition:
goto_model.h:22
goto_model.h
Symbol Table + CFG.
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:517
symbol_tablet
The symbol table.
Definition:
symbol_table.h:52
message_handlert
Definition:
message.h:20
goto_functionst
Definition:
goto_functions.h:20
goto_programt
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition:
goto_program.h:24
goto-programs
remove_function_pointers.h
Generated by
1.8.14