cprover
Loading...
Searching...
No Matches
remove_function_pointers.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Remove Indirect Function Calls
4
5Author: Daniel Kroening
6
7Date: 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_program.h"
18
19#include <unordered_set>
20
21class goto_functionst;
22class goto_modelt;
23class message_handlert;
24class symbol_tablet;
25
26// remove indirect function calls
27// and replace by case-split
28void remove_function_pointers(
29 message_handlert &_message_handler,
30 goto_modelt &goto_model,
31 bool only_remove_const_fps);
32
42void remove_function_pointer(
43 message_handlert &message_handler,
44 symbol_tablet &symbol_table,
45 goto_programt &goto_program,
46 const irep_idt &function_id,
47 goto_programt::targett target,
48 const std::unordered_set<symbol_exprt, irep_hash> &functions);
49
52bool function_is_type_compatible(
53 bool return_value_used,
54 const code_typet &call_type,
55 const code_typet &function_type,
56 const namespacet &ns);
57
60bool has_function_pointers(const goto_functionst &);
61
64bool has_function_pointers(const goto_modelt &);
65
66#endif // CPROVER_GOTO_PROGRAMS_REMOVE_FUNCTION_POINTERS_H
code_typet
Base type of functions.
Definition std_types.h:583
goto_functionst
A collection of goto functions.
Definition goto_functions.h:25
goto_modelt
Definition goto_model.h:27
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition goto_program.h:72
goto_programt::targett
instructionst::iterator targett
Definition goto_program.h:613
message_handlert
Definition message.h:27
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
symbol_tablet
The symbol table.
Definition symbol_table.h:14
goto_program.h
Concrete Goto Program.
has_function_pointers
bool has_function_pointers(const goto_functionst &)
returns true iff any of the given goto functions has function calls via a function pointer
Definition remove_function_pointers.cpp:562
remove_function_pointer
void remove_function_pointer(message_handlert &message_handler, symbol_tablet &symbol_table, goto_programt &goto_program, const irep_idt &function_id, goto_programt::targett target, const std::unordered_set< symbol_exprt, irep_hash > &functions)
Replace a call to a dynamic function at location target in the given goto-program by a case-split ove...
Definition remove_function_pointers.cpp:379
function_is_type_compatible
bool function_is_type_compatible(bool return_value_used, const code_typet &call_type, const code_typet &function_type, const namespacet &ns)
Returns true iff call_type can be converted to produce a function call of the same type as function_t...
Definition remove_function_pointers.cpp:129
remove_function_pointers
void remove_function_pointers(message_handlert &_message_handler, goto_modelt &goto_model, bool only_remove_const_fps)
Definition remove_function_pointers.cpp:535
irep_idt
dstringt irep_idt
Definition verification_result.h:16