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 
13 
14 #ifndef CPROVER_GOTO_PROGRAMS_REMOVE_VIRTUAL_FUNCTIONS_H
15 #define CPROVER_GOTO_PROGRAMS_REMOVE_VIRTUAL_FUNCTIONS_H
16 
17 #include <util/std_expr.h>
18 
19 #include "class_hierarchy.h"
20 #include "goto_program.h"
21 
22 class goto_functionst;
24 class goto_modelt;
25 class symbol_table_baset;
26 
27 // remove virtual function calls
28 // and replace by case-split
30  goto_modelt &goto_model);
31 
33  const symbol_table_baset &symbol_table,
34  goto_functionst &goto_functions);
35 
41 
45 {
52 };
53 
55 {
56  public:
57  dispatch_table_entryt() = default;
58  explicit dispatch_table_entryt(const irep_idt &_class_id) :
59  class_id(_class_id)
60  {}
61 
64 };
65 
66 typedef std::vector<dispatch_table_entryt> dispatch_table_entriest;
67 typedef std::map<irep_idt, dispatch_table_entryt> dispatch_table_entries_mapt;
68 
70  goto_modelt &goto_model,
72  goto_programt::targett instruction,
73  const dispatch_table_entriest &dispatch_table,
74  virtual_dispatch_fallback_actiont fallback_action);
75 
77  symbol_tablet &symbol_table,
79  goto_programt::targett instruction,
80  const dispatch_table_entriest &dispatch_table,
81  virtual_dispatch_fallback_actiont fallback_action);
82 
92  const exprt &function,
93  const symbol_tablet &symbol_table,
94  const class_hierarchyt &class_hierarchy,
95  dispatch_table_entriest &overridden_functions);
96 
97 #endif // CPROVER_GOTO_PROGRAMS_REMOVE_VIRTUAL_FUNCTIONS_H
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:397
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
When no callee type matches, call the last passed function, which is expected to be some safe default...
void remove_virtual_functions(goto_modelt &goto_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:70
Base class for all expressions.
Definition: expr.h:42
The symbol table base class interface.
dispatch_table_entryt()=default
goto_programt & goto_program
Definition: cover.cpp:63
Expression to hold a symbol (variable)
Definition: std_expr.h:90
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:147
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...