cprover
Loading...
Searching...
No Matches
remove_virtual_functions.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Remove Virtual Function (Method) Calls
4
5Author: Daniel Kroening
6
7Date: April 2016
8
9\*******************************************************************/
10
14
15#ifndef CPROVER_GOTO_PROGRAMS_REMOVE_VIRTUAL_FUNCTIONS_H
16#define CPROVER_GOTO_PROGRAMS_REMOVE_VIRTUAL_FUNCTIONS_H
17
18#include <util/optional.h>
19#include <util/std_expr.h>
20
21#include "goto_program.h"
22
23#include <map>
24
26class goto_functionst;
28class goto_modelt;
29class symbol_tablet;
31
32// For all of the following the class-hierarchy and non-class-hierarchy
33// overloads are equivalent, but the class-hierarchy-taking one saves time if
34// you already have a class-hierarchy object available.
35
37 goto_modelt &goto_model);
38
40 goto_modelt &goto_model,
41 const class_hierarchyt &class_hierarchy);
42
44 symbol_table_baset &symbol_table,
45 goto_functionst &goto_functions);
46
48 symbol_table_baset &symbol_table,
49 goto_functionst &goto_functions,
50 const class_hierarchyt &class_hierarchy);
51
53
55 goto_model_functiont &function,
56 const class_hierarchyt &class_hierarchy);
57
61{
68};
69
71{
72public:
73 explicit dispatch_table_entryt(const irep_idt &_class_id)
74 : symbol_expr(), class_id(_class_id)
75 {
76 }
77
78#if defined(__GNUC__) && __GNUC__ < 7
79 // GCC up to version 6.5 warns about irept::data being used uninitialized upon
80 // the move triggered by std::sort; using operator= works around this
82 {
83 symbol_expr = other.symbol_expr;
84 class_id = other.class_id;
85 }
86
87 dispatch_table_entryt &operator=(const dispatch_table_entryt &other)
88 {
90 class_id = other.class_id;
91 return *this;
92 }
93
96 {
97 }
98#endif
99
102};
103
104typedef std::vector<dispatch_table_entryt> dispatch_table_entriest;
105typedef std::map<irep_idt, dispatch_table_entryt> dispatch_table_entries_mapt;
106
108 goto_modelt &goto_model,
109 const irep_idt &function_id,
110 goto_programt &goto_program,
111 goto_programt::targett instruction,
112 const dispatch_table_entriest &dispatch_table,
113 virtual_dispatch_fallback_actiont fallback_action);
114
116 symbol_tablet &symbol_table,
117 const irep_idt &function_id,
118 goto_programt &goto_program,
119 goto_programt::targett instruction,
120 const dispatch_table_entriest &dispatch_table,
121 virtual_dispatch_fallback_actiont fallback_action);
122
132 const exprt &function,
133 const symbol_table_baset &symbol_table,
134 const class_hierarchyt &class_hierarchy,
135 dispatch_table_entriest &overridden_functions);
136
137#endif // CPROVER_GOTO_PROGRAMS_REMOVE_VIRTUAL_FUNCTIONS_H
Non-graph-based representation of the class hierarchy.
dispatch_table_entryt(const irep_idt &_class_id)
optionalt< symbol_exprt > symbol_expr
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
Base class for all expressions.
Definition expr.h:54
A collection of goto functions.
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
Definition goto_model.h:183
A generic container class for the GOTO intermediate representation of one function.
instructionst::iterator targett
The symbol table base class interface.
The symbol table.
Concrete Goto Program.
nonstd::optional< T > optionalt
Definition optional.h:35
void remove_virtual_functions(goto_modelt &goto_model)
Remove virtual function calls from the specified model.
std::map< irep_idt, dispatch_table_entryt > dispatch_table_entries_mapt
void collect_virtual_function_callees(const exprt &function, const symbol_table_baset &symbol_table, const class_hierarchyt &class_hierarchy, dispatch_table_entriest &overridden_functions)
Given a function expression representing a virtual method of a class, the function computes all overr...
virtual_dispatch_fallback_actiont
Specifies remove_virtual_function's behaviour when the actual supplied parameter does not match any o...
@ ASSUME_FALSE
When no callee type matches, ASSUME false, thus preventing any complete trace from using this path.
@ CALL_LAST_FUNCTION
When no callee type matches, call the last passed function, which is expected to be some safe default...
std::vector< dispatch_table_entryt > dispatch_table_entriest
goto_programt::targett remove_virtual_function(goto_modelt &goto_model, const irep_idt &function_id, goto_programt &goto_program, goto_programt::targett instruction, const dispatch_table_entriest &dispatch_table, virtual_dispatch_fallback_actiont fallback_action)
API to expression classes.