cprover
|
Public Member Functions | |
remove_virtual_functionst (const symbol_table_baset &_symbol_table, const class_hierarchyt &_class_hierarchy) | |
void | operator() (goto_functionst &goto_functions) |
bool | remove_virtual_functions (goto_programt &goto_program) |
goto_programt::targett | remove_virtual_function (goto_programt &goto_program, goto_programt::targett target, const dispatch_table_entriest &functions, virtual_dispatch_fallback_actiont fallback_action) |
void | get_functions (const exprt &, dispatch_table_entriest &) |
Used to get dispatch entries to call for the given function. More... | |
Protected Types | |
typedef std::function< resolve_inherited_componentt::inherited_componentt(const irep_idt &, const irep_idt &)> | function_call_resolvert |
Protected Member Functions | |
goto_programt::targett | remove_virtual_function (goto_programt &goto_program, goto_programt::targett target) |
void | get_child_functions_rec (const irep_idt &, const symbol_exprt &, const irep_idt &, dispatch_table_entriest &, dispatch_table_entries_mapt &, const function_call_resolvert &) const |
Used by get_functions to track the most-derived parent that provides an override of a given function. More... | |
exprt | get_method (const irep_idt &class_id, const irep_idt &component_name) const |
Protected Attributes | |
const namespacet | ns |
const symbol_table_baset & | symbol_table |
const class_hierarchyt & | class_hierarchy |
Definition at line 22 of file remove_virtual_functions.cpp.
|
protected |
Definition at line 54 of file remove_virtual_functions.cpp.
remove_virtual_functionst::remove_virtual_functionst | ( | const symbol_table_baset & | _symbol_table, |
const class_hierarchyt & | _class_hierarchy | ||
) |
Definition at line 66 of file remove_virtual_functions.cpp.
|
protected |
Used by get_functions to track the most-derived parent that provides an override of a given function.
parameters | this_id : class name |
<tt>last_method_defn</tt> | the most-derived parent of this_id to define the requested function |
<tt>component_name</tt> | name of the function searched for |
<tt>entry_map</tt> | map of class identifiers to dispatch table entries |
<tt>resolve_function_call</tt> | function to resolve abstract method call |
functions
is assigned a list of {class name, function symbol} pairs indicating that if this
is of the given class, then the call will target the given function. Thus if A <: B <: C and A and C provide overrides of f
(but B does not), get_child_functions_rec("C", C.f, "f") -> [{"C", C.f}, {"B", C.f}, {"A", A.f}] Definition at line 315 of file remove_virtual_functions.cpp.
References class_hierarchy, class_hierarchyt::class_map, resolve_inherited_componentt::inherited_componentt::get_class_identifier(), resolve_inherited_componentt::inherited_componentt::get_full_component_identifier(), get_method(), has_prefix(), id2string(), irept::is_not_nil(), resolve_inherited_componentt::inherited_componentt::is_valid(), symbol_table_baset::lookup_ref(), irept::set(), dispatch_table_entryt::symbol_expr, symbolt::symbol_expr(), symbol_table, and to_symbol_expr().
Referenced by get_functions().
void remove_virtual_functionst::get_functions | ( | const exprt & | function, |
dispatch_table_entriest & | functions | ||
) |
Used to get dispatch entries to call for the given function.
function | function that should be called | |
[out] | functions | is assigned a list of dispatch entries, i.e., pairs of class names and function symbol to call when encountering the class. |
Definition at line 384 of file remove_virtual_functions.cpp.
References class_hierarchy, dispatch_table_entryt::class_id, dstringt::compare(), dstringt::empty(), get_child_functions_rec(), resolve_inherited_componentt::inherited_componentt::get_class_identifier(), resolve_inherited_componentt::inherited_componentt::get_full_component_identifier(), symbol_exprt::get_identifier(), has_prefix(), id2string(), INVARIANT, resolve_inherited_componentt::inherited_componentt::is_valid(), symbol_table_baset::lookup_ref(), irept::set(), dispatch_table_entryt::symbol_expr, symbolt::symbol_expr(), and symbol_table.
Referenced by collect_virtual_function_callees(), and remove_virtual_function().
|
protected |
Definition at line 467 of file remove_virtual_functions.cpp.
References resolve_inherited_componentt::build_full_component_identifier(), namespacet::lookup(), ns, and symbolt::symbol_expr().
Referenced by get_child_functions_rec().
void remove_virtual_functionst::operator() | ( | goto_functionst & | goto_functions | ) |
Definition at line 514 of file remove_virtual_functions.cpp.
References goto_functionst::compute_location_numbers(), goto_functionst::function_map, goto_program, and remove_virtual_functions().
goto_programt::targett remove_virtual_functionst::remove_virtual_function | ( | goto_programt & | goto_program, |
goto_programt::targett | target, | ||
const dispatch_table_entriest & | functions, | ||
virtual_dispatch_fallback_actiont | fallback_action | ||
) |
Definition at line 122 of file remove_virtual_functions.cpp.
References goto_programt::add_instruction(), ASSUME, ASSUME_FALSE, CALL_LAST_FUNCTION, comment(), create_static_function_call(), goto_programt::destructive_append(), goto_programt::destructive_insert(), dstringt::empty(), goto_programt::empty(), Forall_goto_program_instructions, get_class_identifier_field(), goto_program, irept::id(), id2string(), goto_programt::instructions, INVARIANT, ns, remove_skip(), typet::subtype(), to_code_function_call(), and exprt::type().
Referenced by remove_virtual_function(), remove_virtual_function(), and remove_virtual_functions().
|
protected |
Definition at line 75 of file remove_virtual_functions.cpp.
References code_function_callt::arguments(), CALL_LAST_FUNCTION, code_function_callt::function(), get_functions(), goto_program, INVARIANT, remove_virtual_function(), and to_code_function_call().
bool remove_virtual_functionst::remove_virtual_functions | ( | goto_programt & | goto_program | ) |
Definition at line 482 of file remove_virtual_functions.cpp.
References code_function_callt::function(), goto_program, irept::id(), goto_programt::instructions, remove_virtual_function(), to_code_function_call(), and goto_programt::update().
Referenced by operator()(), and remove_virtual_functions().
|
protected |
Definition at line 45 of file remove_virtual_functions.cpp.
Referenced by get_child_functions_rec(), and get_functions().
|
protected |
Definition at line 42 of file remove_virtual_functions.cpp.
Referenced by get_method(), and remove_virtual_function().
|
protected |
Definition at line 43 of file remove_virtual_functions.cpp.
Referenced by get_child_functions_rec(), and get_functions().