cprover
|
Classes | |
class | arg_stackt |
Public Member Functions | |
const_function_pointer_propagationt (symbol_tablet &_symbol_table, goto_functionst &_goto_functions, messaget &_message) | |
void | propagate () |
Protected Member Functions | |
bool | resolve (const irep_idt &symb, symbol_exprt &goto_function, unsigned &stack_scope) |
bool | add (const irep_idt &symb, const symbol_exprt &goto_function) |
bool | add (const irep_idt &symb, const symbol_exprt &goto_function, unsigned scope) |
bool | remove (const irep_idt &symb) |
bool | has (const irep_idt &symb) const |
symbol_exprt | get (const irep_idt &symb) |
void | propagate (const irep_idt &function) |
void | dup_caller_and_inline_callee (const symbol_exprt &function, unsigned stack_scope) |
Protected Attributes | |
symbol_tablet & | symbol_table |
goto_functionst & | goto_functions |
const namespacet | ns |
messaget & | message |
std::unordered_map< irep_idt, unsigned, irep_id_hash > | map_unique |
std::unordered_map< irep_idt, symbol_exprt, irep_id_hash > | pointer_to_fun |
std::unordered_map< irep_idt, unsigned, irep_id_hash > | pointer_to_stack |
std::unordered_map< irep_idt, unsigned, irep_id_hash > | fun_id_to_invok |
goto_programt::const_targetst | callsite_stack |
std::set< irep_idt > | functions_met |
Definition at line 28 of file propagate_const_function_pointers.cpp.
|
inline |
Definition at line 132 of file propagate_const_function_pointers.cpp.
|
inlineprotected |
Definition at line 72 of file propagate_const_function_pointers.cpp.
References callsite_stack.
Referenced by const_function_pointer_propagationt::arg_stackt::add_args(), and propagate().
|
inlineprotected |
Definition at line 77 of file propagate_const_function_pointers.cpp.
References symbolt::base_name, fun_id_to_invok, symbol_exprt::get_identifier(), namespacet::lookup(), ns, pointer_to_fun, and pointer_to_stack.
|
protected |
Definition at line 150 of file propagate_const_function_pointers.cpp.
References symbol_tablet::add(), code_function_callt::arguments(), symbolt::base_name, goto_function_templatet< bodyT >::body, callsite_stack, goto_function_templatet< bodyT >::copy_from(), messaget::debug(), messaget::eom(), code_function_callt::function(), goto_functions_templatet< bodyT >::function_map, symbol_exprt::get_identifier(), goto_functions, irept::id(), id2string(), namespacet::lookup(), map_unique, message, symbolt::name, ns, address_of_exprt::object(), code_typet::parameters(), pointer_to_fun, symbolt::pretty_name, messaget::mstreamt::source_location, symbol_table, to_address_of_expr(), to_code_function_call(), to_symbol_expr(), goto_function_templatet< bodyT >::type, and goto_functions_templatet< bodyT >::update().
Referenced by propagate().
|
inlineprotected |
Definition at line 103 of file propagate_const_function_pointers.cpp.
References pointer_to_fun.
Referenced by const_function_pointer_propagationt::arg_stackt::add_args().
|
inlineprotected |
Definition at line 98 of file propagate_const_function_pointers.cpp.
References pointer_to_fun.
Referenced by const_function_pointer_propagationt::arg_stackt::add_args().
|
protected |
Definition at line 425 of file propagate_const_function_pointers.cpp.
References add(), const_function_pointer_propagationt::arg_stackt::add_args(), symbolt::base_name, callsite_stack, messaget::debug(), dup_caller_and_inline_callee(), messaget::eom(), Forall_goto_program_instructions, code_function_callt::function(), goto_functions_templatet< bodyT >::function_map, functions_met, symbol_exprt::get_identifier(), goto_functions, irept::id(), code_assignt::lhs(), symbol_tablet::lookup(), message, address_of_exprt::object(), dereference_exprt::pointer(), propagate(), const_function_pointer_propagationt::arg_stackt::remove_args(), resolve(), code_assignt::rhs(), symbol_table, to_address_of_expr(), to_code_assign(), to_code_function_call(), to_dereference_expr(), to_symbol_expr(), and exprt::type().
Referenced by propagate_const_function_pointers().
|
inline |
Definition at line 140 of file propagate_const_function_pointers.cpp.
References goto_functions_templatet< goto_programt >::entry_point().
Referenced by propagate().
|
inlineprotected |
Definition at line 91 of file propagate_const_function_pointers.cpp.
References pointer_to_fun.
|
inlineprotected |
Definition at line 50 of file propagate_const_function_pointers.cpp.
References messaget::debug(), messaget::eom(), message, pointer_to_fun, and pointer_to_stack.
Referenced by propagate().
|
protected |
Definition at line 48 of file propagate_const_function_pointers.cpp.
Referenced by add(), dup_caller_and_inline_callee(), and propagate().
|
protected |
Definition at line 45 of file propagate_const_function_pointers.cpp.
Referenced by add(), and const_function_pointer_propagationt::arg_stackt::add_args().
|
protected |
Definition at line 109 of file propagate_const_function_pointers.cpp.
Referenced by propagate().
|
protected |
Definition at line 32 of file propagate_const_function_pointers.cpp.
Referenced by const_function_pointer_propagationt::arg_stackt::add_args(), dup_caller_and_inline_callee(), propagate(), and propagate_const_function_pointers().
|
protected |
Definition at line 36 of file propagate_const_function_pointers.cpp.
Referenced by dup_caller_and_inline_callee().
|
protected |
Definition at line 34 of file propagate_const_function_pointers.cpp.
Referenced by const_function_pointer_propagationt::arg_stackt::add_args(), dup_caller_and_inline_callee(), propagate(), propagate_const_function_pointers(), and resolve().
|
protected |
Definition at line 33 of file propagate_const_function_pointers.cpp.
Referenced by add(), and dup_caller_and_inline_callee().
|
protected |
Definition at line 39 of file propagate_const_function_pointers.cpp.
Referenced by add(), dup_caller_and_inline_callee(), get(), has(), remove(), and resolve().
|
protected |
Definition at line 42 of file propagate_const_function_pointers.cpp.
|
protected |
Definition at line 31 of file propagate_const_function_pointers.cpp.
Referenced by const_function_pointer_propagationt::arg_stackt::add_args(), dup_caller_and_inline_callee(), propagate(), and propagate_const_function_pointers().