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;
30
31// For all of the following the class-hierarchy and non-class-hierarchy
32// overloads are equivalent, but the class-hierarchy-taking one saves time if
33// you already have a class-hierarchy object available.
34
36 goto_modelt &goto_model);
37
39 goto_modelt &goto_model,
40 const class_hierarchyt &class_hierarchy);
41
43 symbol_table_baset &symbol_table,
44 goto_functionst &goto_functions);
45
47 symbol_table_baset &symbol_table,
48 goto_functionst &goto_functions,
49 const class_hierarchyt &class_hierarchy);
50
52
54 goto_model_functiont &function,
55 const class_hierarchyt &class_hierarchy);
56
68
70{
71public:
72 explicit dispatch_table_entryt(const irep_idt &_class_id)
73 : symbol_expr(), class_id(_class_id)
74 {
75 }
76
77#if defined(__GNUC__) && __GNUC__ < 7
78 // GCC up to version 6.5 warns about irept::data being used uninitialized upon
79 // the move triggered by std::sort; using operator= works around this
81 {
82 symbol_expr = other.symbol_expr;
83 class_id = other.class_id;
84 }
85
86 dispatch_table_entryt &operator=(const dispatch_table_entryt &other)
87 {
89 class_id = other.class_id;
90 return *this;
91 }
92
95 {
96 }
97#endif
98
101};
102
103typedef std::vector<dispatch_table_entryt> dispatch_table_entriest;
104typedef std::map<irep_idt, dispatch_table_entryt> dispatch_table_entries_mapt;
105
107 goto_modelt &goto_model,
108 const irep_idt &function_id,
109 goto_programt &goto_program,
110 goto_programt::targett instruction,
111 const dispatch_table_entriest &dispatch_table,
112 virtual_dispatch_fallback_actiont fallback_action);
113
115 symbol_table_baset &symbol_table,
116 const irep_idt &function_id,
117 goto_programt &goto_program,
118 goto_programt::targett instruction,
119 const dispatch_table_entriest &dispatch_table,
120 virtual_dispatch_fallback_actiont fallback_action);
121
131 const exprt &function,
132 const symbol_table_baset &symbol_table,
133 const class_hierarchyt &class_hierarchy,
134 dispatch_table_entriest &overridden_functions);
135
136#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:39
Base class for all expressions.
Definition expr.h:56
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:190
A generic container class for the GOTO intermediate representation of one function.
instructionst::iterator targett
The symbol table base class interface.
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.