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
27
void
remove_function_pointers
(
28
message_handlert
&_message_handler,
29
goto_modelt
&goto_model,
30
bool
add_safety_assertion,
31
bool
only_remove_const_fps=
false
);
32
33
void
remove_function_pointers
(
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
40
bool
remove_function_pointers
(
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
goto-programs
remove_function_pointers.h
Generated by
1.8.20