Loading...

Searching...

No Matches

Classes | Typedefs | Enumerations | Functions

remove_virtual_functions.h File Reference

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.

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

Remove virtual function calls from the specified model.

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.

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.

void remove_virtual_functions (goto_model_functiont &function)

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

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.

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.

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.

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 class 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 846 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 829 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 808 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 765 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 781 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 742 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 753 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 714 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 731 of file remove_virtual_functions.cpp.