CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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;
24class symbol_tablet;
25
26// remove indirect function calls
27// and replace by case-split
30 goto_modelt &goto_model,
32
43 message_handlert &message_handler,
44 symbol_tablet &symbol_table,
45 goto_programt &goto_program,
46 const irep_idt &function_id,
48 const std::unordered_set<symbol_exprt, irep_hash> &functions);
49
54 const code_typet &call_type,
55 const code_typet &function_type,
56 const namespacet &ns);
57
61
65
66#endif // CPROVER_GOTO_PROGRAMS_REMOVE_FUNCTION_POINTERS_H
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Base type of functions.
Definition std_types.h:583
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:38
A collection of goto functions.
A generic container class for the GOTO intermediate representation of one function.
instructionst::iterator targett
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The symbol table.
Concrete Goto Program.
bool has_function_pointers(const goto_functionst &)
returns true iff any of the given goto functions has function calls via a 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...
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...
void remove_function_pointers(message_handlert &_message_handler, goto_modelt &goto_model, bool only_remove_const_fps)