15 #ifndef CPROVER_GOTO_PROGRAMS_REMOVE_VIRTUAL_FUNCTIONS_H 16 #define CPROVER_GOTO_PROGRAMS_REMOVE_VIRTUAL_FUNCTIONS_H 91 const exprt &
function,
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's behaviour when the actual supplied parameter does not match any o...
instructionst::iterator targett
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...
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...
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.
Base class for all expressions.
The symbol table base class interface.
dispatch_table_entryt()=default
Expression to hold a symbol (variable)
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)
Interface providing access to a single function in a GOTO model, plus its associated symbol table...
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...