Go to the documentation of this file.
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
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
When no callee type matches, call the last passed function, which is expected to be some safe default...
virtual_dispatch_fallback_actiont
Specifies remove_virtual_function's behaviour when the actual supplied parameter does not match any o...
Non-graph-based representation of the class hierarchy.
When no callee type matches, ASSUME false, thus preventing any complete trace from using this path.
Base class for all expressions.
std::vector< dispatch_table_entryt > dispatch_table_entriest
Expression to hold a symbol (variable)
dispatch_table_entryt(const irep_idt &_class_id)
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)
The symbol table base class interface.
dispatch_table_entryt()=default
std::map< irep_idt, dispatch_table_entryt > dispatch_table_entries_mapt
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...
A collection of goto functions.
void remove_virtual_functions(goto_modelt &goto_model)
Remove virtual function calls from the specified model.
A generic container class for the GOTO intermediate representation of one function.
Interface providing access to a single function in a GOTO model, plus its associated symbol table.
instructionst::iterator targett