cprover
remove_virtual_functions.cpp File Reference
#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"
+ Include dependency graph for remove_virtual_functions.cpp:

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)
 

Detailed Description

Remove Virtual Function (Method) Calls

Definition in file remove_virtual_functions.cpp.

Function Documentation

◆ collect_virtual_function_callees()

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.

◆ create_static_function_call()

static void create_static_function_call ( code_function_callt call,
const symbol_exprt function_symbol,
const namespacet ns 
)
static

Create a concrete function call to replace a virtual one.

Parameters
call[in,out]: the function call to update
function_symbolthe function to be called
nsnamespace

Definition at line 111 of file remove_virtual_functions.cpp.

◆ remove_virtual_function() [1/2]

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.

◆ remove_virtual_function() [2/2]

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)

Parameters
symbol_tableSymbol table
goto_program[in/out]: GOTO program to modify
instructionIterator to the GOTO instruction in the supplied GOTO program to be removed. Must point to a function call
dispatch_tableDispatch 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
Returns
Returns a pointer to the statement in the supplied GOTO program after replaced function call

Definition at line 610 of file remove_virtual_functions.cpp.

◆ remove_virtual_functions() [1/3]

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.

◆ remove_virtual_functions() [2/3]

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.

◆ remove_virtual_functions() [3/3]

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.