cprover
remove_virtual_functions.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Remove Virtual Function (Method) Calls
4 
5 Author: Daniel Kroening
6 
7 Date: 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 "class_hierarchy.h"
22 #include "goto_program.h"
23 
24 class goto_functionst;
26 class goto_modelt;
27 class symbol_table_baset;
28 
29 // For all of the following the class-hierarchy and non-class-hierarchy
30 // overloads are equivalent, but the class-hierarchy-taking one saves time if
31 // you already have a class-hierarchy object available.
32 
34  goto_modelt &goto_model);
35 
37  goto_modelt &goto_model,
38  const class_hierarchyt &class_hierarchy);
39 
41  symbol_table_baset &symbol_table,
42  goto_functionst &goto_functions);
43 
45  symbol_table_baset &symbol_table,
46  goto_functionst &goto_functions,
47  const class_hierarchyt &class_hierarchy);
48 
50 
52  goto_model_functiont &function,
53  const class_hierarchyt &class_hierarchy);
54 
58 {
65 };
66 
68 {
69 public:
70  explicit dispatch_table_entryt(const irep_idt &_class_id)
71  : symbol_expr(), class_id(_class_id)
72  {
73  }
74 
75 #if defined(__GNUC__) && __GNUC__ < 7
76  // GCC up to version 6.5 warns about irept::data being used uninitialized upon
77  // the move triggered by std::sort; using operator= works around this
79  {
80  symbol_expr = other.symbol_expr;
81  class_id = other.class_id;
82  }
83 
84  dispatch_table_entryt &operator=(const dispatch_table_entryt &other)
85  {
86  symbol_expr = other.symbol_expr;
87  class_id = other.class_id;
88  return *this;
89  }
90 
92  : symbol_expr(other.symbol_expr), class_id(other.class_id)
93  {
94  }
95 #endif
96 
99 };
100 
101 typedef std::vector<dispatch_table_entryt> dispatch_table_entriest;
102 typedef std::map<irep_idt, dispatch_table_entryt> dispatch_table_entries_mapt;
103 
105  goto_modelt &goto_model,
106  const irep_idt &function_id,
107  goto_programt &goto_program,
108  goto_programt::targett instruction,
109  const dispatch_table_entriest &dispatch_table,
110  virtual_dispatch_fallback_actiont fallback_action);
111 
113  symbol_tablet &symbol_table,
114  const irep_idt &function_id,
115  goto_programt &goto_program,
116  goto_programt::targett instruction,
117  const dispatch_table_entriest &dispatch_table,
118  virtual_dispatch_fallback_actiont fallback_action);
119 
129  const exprt &function,
130  const symbol_table_baset &symbol_table,
131  const class_hierarchyt &class_hierarchy,
132  dispatch_table_entriest &overridden_functions);
133 
134 #endif // CPROVER_GOTO_PROGRAMS_REMOVE_VIRTUAL_FUNCTIONS_H
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
virtual_dispatch_fallback_actiont::CALL_LAST_FUNCTION
@ CALL_LAST_FUNCTION
When no callee type matches, call the last passed function, which is expected to be some safe default...
virtual_dispatch_fallback_actiont
virtual_dispatch_fallback_actiont
Specifies remove_virtual_function's behaviour when the actual supplied parameter does not match any o...
Definition: remove_virtual_functions.h:58
dispatch_table_entryt
Definition: remove_virtual_functions.h:68
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
class_hierarchyt
Non-graph-based representation of the class hierarchy.
Definition: class_hierarchy.h:43
virtual_dispatch_fallback_actiont::ASSUME_FALSE
@ ASSUME_FALSE
When no callee type matches, ASSUME false, thus preventing any complete trace from using this path.
optional.h
dispatch_table_entryt::class_id
irep_idt class_id
Definition: remove_virtual_functions.h:98
exprt
Base class for all expressions.
Definition: expr.h:53
goto_modelt
Definition: goto_model.h:26
dispatch_table_entriest
std::vector< dispatch_table_entryt > dispatch_table_entriest
Definition: remove_virtual_functions.h:101
dispatch_table_entryt::dispatch_table_entryt
dispatch_table_entryt(const irep_idt &_class_id)
Definition: remove_virtual_functions.h:70
symbol_table_baset
The symbol table base class interface.
Definition: symbol_table_base.h:22
collect_virtual_function_callees
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...
Definition: remove_virtual_functions.cpp:855
dispatch_table_entryt::symbol_expr
optionalt< symbol_exprt > symbol_expr
Definition: remove_virtual_functions.h:97
dispatch_table_entries_mapt
std::map< irep_idt, dispatch_table_entryt > dispatch_table_entries_mapt
Definition: remove_virtual_functions.h:102
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
goto_program.h
Concrete Goto Program.
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
class_hierarchy.h
Class Hierarchy.
remove_virtual_functions
void remove_virtual_functions(goto_modelt &goto_model)
Remove virtual function calls from the specified model.
Definition: remove_virtual_functions.cpp:751
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
std_expr.h
API to expression classes.
goto_model_functiont
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
Definition: goto_model.h:183
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:579
remove_virtual_function
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)
Definition: remove_virtual_functions.cpp:838