cprover
remove_virtual_functions.h File Reference

Remove Virtual Function (Method) Calls. More...

#include <util/std_expr.h>
#include "class_hierarchy.h"
#include "goto_program.h"
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_entrytdispatch_table_entriest
 
typedef std::map< irep_idt, dispatch_table_entrytdispatch_table_entries_mapt
 

Enumerations

enum  virtual_dispatch_fallback_actiont { virtual_dispatch_fallback_actiont::CALL_LAST_FUNCTION, virtual_dispatch_fallback_actiont::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)
 
void remove_virtual_functions (const symbol_table_baset &symbol_table, goto_functionst &goto_functions)
 
void remove_virtual_functions (goto_model_functiont &function)
 Remove virtual functions from one function. 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)
 
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)
 
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 overridden methods of that virtual method. More...
 

Detailed Description

Remove Virtual Function (Method) Calls.

Definition in file remove_virtual_functions.h.

Typedef Documentation

◆ dispatch_table_entries_mapt

◆ dispatch_table_entriest

Definition at line 66 of file remove_virtual_functions.h.

Enumeration Type Documentation

◆ virtual_dispatch_fallback_actiont

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 44 of file remove_virtual_functions.h.

Function Documentation

◆ collect_virtual_function_callees()

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 overridden methods of that virtual method.

Parameters
functionThe virtual function expression for which the overridden methods will be searched for.
symbol_tableA symbol table.
class_hierarchyA class hierarchy.
[out]overridden_functionsOutput collection into which all overridden functions will be stored.

◆ 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 
)

◆ 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 
)

◆ remove_virtual_functions() [1/3]

void remove_virtual_functions ( goto_modelt goto_model)

◆ remove_virtual_functions() [2/3]

◆ remove_virtual_functions() [3/3]

void remove_virtual_functions ( goto_model_functiont function)

Remove virtual functions from one function.

May change the location numbers in function.

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

Definition at line 549 of file remove_virtual_functions.cpp.

References remove_virtual_functionst::remove_virtual_functions().