Functions for replacing virtual function call with a static function calls in functions, groups of functions and goto programs. More...

#include <util/std_expr.h>
#include "goto_program.h"
#include <map>

Include dependency graph for remove_virtual_functions.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes
class	dispatch_table_entryt

Typedefs
typedef std::vector< dispatch_table_entryt >	dispatch_table_entriest

typedef std::map< irep_idt, dispatch_table_entryt >	dispatch_table_entries_mapt

Enumerations
enum class	virtual_dispatch_fallback_actiont { CALL_LAST_FUNCTION , ASSUME_FALSE }
	Specifies remove_virtual_function's behaviour when the actual supplied parameter does not match any of the possible callee types. More...

Functions
void	remove_virtual_functions (goto_modelt &goto_model)
	Remove virtual function calls from the specified model. More...

void	remove_virtual_functions (goto_modelt &goto_model, const class_hierarchyt &class_hierarchy)
	Remove virtual function calls from the specified model. More...

void	remove_virtual_functions (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 (symbol_table_baset &symbol_table, goto_functionst &goto_functions, const class_hierarchyt &class_hierarchy)
	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_model_functiont &function)
	Remove virtual function calls from the specified model function May change the location numbers in `function`. More...

void	remove_virtual_functions (goto_model_functiont &function, const class_hierarchyt &class_hierarchy)
	Remove virtual function calls from the specified model function May change the location numbers in `function`. More...

goto_programt::targett	remove_virtual_function (goto_modelt &goto_model, const irep_idt &function_id, goto_programt &goto_program, goto_programt::targett instruction, const dispatch_table_entriest &dispatch_table, virtual_dispatch_fallback_actiont fallback_action)

goto_programt::targett	remove_virtual_function (symbol_table_baset &symbol_table, const irep_idt &function_id, 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...

void	collect_virtual_function_callees (const exprt &function, const symbol_table_baset &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 overridden methods of that virtual method. More...

Detailed Description

Functions for replacing virtual function call with a static function calls in functions, groups of functions and goto programs.

Definition in file remove_virtual_functions.h.

Typedef Documentation

◆ dispatch_table_entries_mapt

typedef std::map<irep_idt, dispatch_table_entryt> dispatch_table_entries_mapt

Definition at line 103 of file remove_virtual_functions.h.

◆ dispatch_table_entriest

typedef std::vector<dispatch_table_entryt> dispatch_table_entriest

Definition at line 102 of file remove_virtual_functions.h.

Enumeration Type Documentation

◆ virtual_dispatch_fallback_actiont

enum virtual_dispatch_fallback_actiont

strong

Specifies remove_virtual_function's behaviour when the actual supplied parameter does not match any of the possible callee types.

Enumerator
CALL_LAST_FUNCTION	When no callee type matches, call the last passed function, which is expected to be some safe default:
ASSUME_FALSE	When no callee type matches, ASSUME false, thus preventing any complete trace from using this path.

Definition at line 58 of file remove_virtual_functions.h.

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
	)

Given a function expression representing a virtual method of a class, the function computes all overridden methods of that virtual method.

Parameters

	function	The virtual function expression for which the overridden methods will be searched for.
	symbol_table	A symbol table.
	class_hierarchy	A class hierarchy.
[out]	overridden_functions	Output collection into which all overridden functions will be stored.

Definition at line 848 of file remove_virtual_functions.cpp.

◆ remove_virtual_function() [1/2]

goto_programt::targett remove_virtual_function	(	goto_modelt &	goto_model,
		const irep_idt &	function_id,
		goto_programt &	goto_program,
		goto_programt::targett	instruction,
		const dispatch_table_entriest &	dispatch_table,
		virtual_dispatch_fallback_actiont	fallback_action
	)

Definition at line 831 of file remove_virtual_functions.cpp.

◆ remove_virtual_function() [2/2]

goto_programt::targett remove_virtual_function	(	symbol_table_baset &	symbol_table,
		const irep_idt &	function_id,
		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_table	Symbol table
	function_id	The identifier of the function we are currently analysing
[in,out]	goto_program	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

Returns: Returns a pointer to the statement in the supplied GOTO program after replaced function call

Definition at line 810 of file remove_virtual_functions.cpp.

◆ remove_virtual_functions() [1/6]

void remove_virtual_functions ( goto_model_functiont & function )

Remove virtual function calls from the specified model function May change the location numbers in function.

Parameters

function function from which virtual functions should be converted to explicit dispatch tables.

Definition at line 767 of file remove_virtual_functions.cpp.

◆ remove_virtual_functions() [2/6]

void remove_virtual_functions	(	goto_model_functiont &	function,
		const class_hierarchyt &	class_hierarchy
	)

Remove virtual function calls from the specified model function May change the location numbers in function.

Parameters

function	function from which virtual functions should be converted to explicit dispatch tables.
class_hierarchy	class hierarchy derived from function.symbol_table This should already be populated (i.e. class_hierarchyt::operator() has already been called)

Definition at line 783 of file remove_virtual_functions.cpp.

◆ remove_virtual_functions() [3/6]

void remove_virtual_functions ( goto_modelt & goto_model )

Remove virtual function calls from the specified model.

Parameters

goto_model model from which to remove virtual functions

Definition at line 744 of file remove_virtual_functions.cpp.

◆ remove_virtual_functions() [4/6]

void remove_virtual_functions	(	goto_modelt &	goto_model,
		const class_hierarchyt &	class_hierarchy
	)

Remove virtual function calls from the specified model.

Parameters

goto_model	model from which to remove virtual functions
class_hierarchy	class hierarchy derived from model.symbol_table This should already be populated (i.e. class_hierarchyt::operator() has already been called)

Definition at line 755 of file remove_virtual_functions.cpp.

◆ remove_virtual_functions() [5/6]

void remove_virtual_functions	(	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.

Parameters

symbol_table	symbol table associated with `goto_functions`
goto_functions	functions from which to remove virtual function calls

Definition at line 716 of file remove_virtual_functions.cpp.

◆ remove_virtual_functions() [6/6]

void remove_virtual_functions	(	symbol_table_baset &	symbol_table,
		goto_functionst &	goto_functions,
		const class_hierarchyt &	class_hierarchy
	)

Remove virtual function calls from all functions in the specified list and replace them with their most derived implementations.

Parameters

symbol_table	symbol table associated with `goto_functions`
goto_functions	functions from which to remove virtual function calls
class_hierarchy	class hierarchy derived from symbol_table This should already be populated (i.e. class_hierarchyt::operator() has already been called)

Definition at line 733 of file remove_virtual_functions.cpp.

Classes

Typedefs

Enumerations

Functions

Detailed Description

Typedef Documentation

◆ dispatch_table_entries_mapt

◆ dispatch_table_entriest

Enumeration Type Documentation

◆ virtual_dispatch_fallback_actiont

Function Documentation

◆ collect_virtual_function_callees()

◆ remove_virtual_function() [1/2]

◆ remove_virtual_function() [2/2]

◆ remove_virtual_functions() [1/6]

◆ remove_virtual_functions() [2/6]

◆ remove_virtual_functions() [3/6]

◆ remove_virtual_functions() [4/6]

◆ remove_virtual_functions() [5/6]

◆ remove_virtual_functions() [6/6]