cprover
|
Remove Virtual Function (Method) Calls. More...
#include "remove_virtual_functions.h"
#include <algorithm>
#include <util/type_eq.h>
#include "class_identifier.h"
#include "goto_model.h"
#include "remove_skip.h"
#include "resolve_inherited_component.h"
Go to the source code of this file.
Classes | |
class | remove_virtual_functionst |
Functions | |
static void | create_static_function_call (code_function_callt &call, const symbol_exprt &function_symbol, const namespacet &ns) |
Create a concrete function call to replace a virtual one. More... | |
void | remove_virtual_functions (const symbol_table_baset &symbol_table, goto_functionst &goto_functions) |
Remove virtual function calls from all functions in the specified list and replace them with their most derived implementations. More... | |
void | remove_virtual_functions (goto_modelt &goto_model) |
Remove virtual function calls from the specified model. More... | |
void | remove_virtual_functions (goto_model_functiont &function) |
Remove virtual function calls from the specified model function. More... | |
goto_programt::targett | remove_virtual_function (symbol_tablet &symbol_table, goto_programt &goto_program, goto_programt::targett instruction, const dispatch_table_entriest &dispatch_table, virtual_dispatch_fallback_actiont fallback_action) |
Replace virtual function call with a static function call Achieved by substituting a virtual function with its most derived implementation. More... | |
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) |
void | collect_virtual_function_callees (const exprt &function, const symbol_table_baset &symbol_table, const class_hierarchyt &class_hierarchy, dispatch_table_entriest &overridden_functions) |
Remove Virtual Function (Method) Calls.
Definition in file remove_virtual_functions.cpp.
void collect_virtual_function_callees | ( | const exprt & | function, |
const symbol_table_baset & | symbol_table, | ||
const class_hierarchyt & | class_hierarchy, | ||
dispatch_table_entriest & | overridden_functions | ||
) |
Definition at line 644 of file remove_virtual_functions.cpp.
|
static |
Create a concrete function call to replace a virtual one.
call | [in,out]: the function call to update |
function_symbol | the function to be called |
ns | namespace |
Definition at line 111 of file remove_virtual_functions.cpp.
goto_programt::targett remove_virtual_function | ( | symbol_tablet & | symbol_table, |
goto_programt & | goto_program, | ||
goto_programt::targett | instruction, | ||
const dispatch_table_entriest & | dispatch_table, | ||
virtual_dispatch_fallback_actiont | fallback_action | ||
) |
Replace virtual function call with a static function call Achieved by substituting a virtual function with its most derived implementation.
If there's a type mismatch between implementation and the instance type or if fallback_action is set to ASSUME_FALSE, then function is substituted with a call to ASSUME(false)
symbol_table | Symbol table |
goto_program | [in/out]: GOTO program to modify |
instruction | Iterator to the GOTO instruction in the supplied GOTO program to be removed. Must point to a function call |
dispatch_table | Dispatch table - all possible implementations of this function sorted from the least to the most derived |
fallback_action | - ASSUME_FALSE to replace virtual function calls with ASSUME(false) or CALL_LAST_FUNCTION to replace them with the most derived matching call |
Definition at line 610 of file remove_virtual_functions.cpp.
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 | ||
) |
Definition at line 629 of file remove_virtual_functions.cpp.
void remove_virtual_functions | ( | const symbol_table_baset & | symbol_table, |
goto_functionst & | goto_functions | ||
) |
Remove virtual function calls from all functions in the specified list and replace them with their most derived implementations.
Definition at line 568 of file remove_virtual_functions.cpp.
void remove_virtual_functions | ( | goto_modelt & | goto_model | ) |
Remove virtual function calls from the specified model.
Definition at line 579 of file remove_virtual_functions.cpp.
void remove_virtual_functions | ( | goto_model_functiont & | function | ) |
Remove virtual function calls from the specified model function.
Remove virtual functions from one function.
Definition at line 586 of file remove_virtual_functions.cpp.