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/std_expr.h>
19 
20 #include "class_hierarchy.h"
21 #include "goto_program.h"
22 
23 class goto_functionst;
25 class goto_modelt;
26 class symbol_table_baset;
27 
29  goto_modelt &goto_model);
30 
32  const symbol_table_baset &symbol_table,
33  goto_functionst &goto_functions);
34 
40 
44 {
51 };
52 
54 {
55  public:
56  dispatch_table_entryt() = default;
57  explicit dispatch_table_entryt(const irep_idt &_class_id) :
58  class_id(_class_id)
59  {}
60 
63 };
64 
65 typedef std::vector<dispatch_table_entryt> dispatch_table_entriest;
66 typedef std::map<irep_idt, dispatch_table_entryt> dispatch_table_entries_mapt;
67 
69  goto_modelt &goto_model,
70  goto_programt &goto_program,
71  goto_programt::targett instruction,
72  const dispatch_table_entriest &dispatch_table,
73  virtual_dispatch_fallback_actiont fallback_action);
74 
76  symbol_tablet &symbol_table,
77  goto_programt &goto_program,
78  goto_programt::targett instruction,
79  const dispatch_table_entriest &dispatch_table,
80  virtual_dispatch_fallback_actiont fallback_action);
81 
91  const exprt &function,
92  const symbol_tablet &symbol_table,
93  const class_hierarchyt &class_hierarchy,
94  dispatch_table_entriest &overridden_functions);
95 
96 #endif // CPROVER_GOTO_PROGRAMS_REMOVE_VIRTUAL_FUNCTIONS_H
Non-graph-based representation of the class hierarchy.
virtual_dispatch_fallback_actiont
Specifies remove_virtual_function&#39;s behaviour when the actual supplied parameter does not match any o...
Class Hierarchy.
instructionst::iterator targett
Definition: goto_program.h:414
std::vector< dispatch_table_entryt > dispatch_table_entriest
API to expression classes.
When no callee type matches, ASSUME false, thus preventing any complete trace from using this path...
The symbol table.
Definition: symbol_table.h:19
A collection of goto functions.
When no callee type matches, call the last passed function, which is expected to be some safe default...
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.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
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
Base class for all expressions.
Definition: expr.h:54
The symbol table base class interface.
dispatch_table_entryt()=default
Expression to hold a symbol (variable)
Definition: std_expr.h:143
goto_programt::targett remove_virtual_function(goto_modelt &goto_model, goto_programt &goto_program, goto_programt::targett instruction, const dispatch_table_entriest &dispatch_table, virtual_dispatch_fallback_actiont fallback_action)
dispatch_table_entryt(const irep_idt &_class_id)
Concrete Goto Program.
Interface providing access to a single function in a GOTO model, plus its associated symbol table...
Definition: goto_model.h:153
void collect_virtual_function_callees(const exprt &function, const symbol_tablet &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...