cprover
|
Public Member Functions | |
remove_returnst (symbol_table_baset &_symbol_table) | |
void | operator() (goto_functionst &goto_functions) |
void | operator() (goto_model_functiont &model_function, function_is_stubt function_is_stub) |
void | restore (goto_functionst &goto_functions) |
Protected Member Functions | |
void | replace_returns (const irep_idt &function_id, goto_functionst::goto_functiont &function) |
turns 'return x' into an assignment to fkt::return_value More... | |
void | do_function_calls (function_is_stubt function_is_stub, goto_programt &goto_program) |
turns x=f(...) into f(...); lhs=f::return_value; More... | |
bool | restore_returns (goto_functionst::function_mapt::iterator f_it) |
turns an assignment to fkt::return_value back into 'return x' More... | |
void | undo_function_calls (goto_functionst &goto_functions, goto_programt &goto_program) |
turns f(...); lhs=f::return_value; into lhs=f(...) More... | |
symbol_exprt | get_or_create_return_value_symbol (const irep_idt &function_id) |
Protected Attributes | |
symbol_table_baset & | symbol_table |
Definition at line 22 of file remove_returns.cpp.
|
inlineexplicit |
Definition at line 25 of file remove_returns.cpp.
|
protected |
turns x=f(...) into f(...); lhs=f::return_value;
function_is_stub | function (irep_idt -> bool) that determines whether a given function ID is a stub |
goto_program | program to transform |
Definition at line 139 of file remove_returns.cpp.
References Forall_goto_program_instructions, code_function_callt::function(), get_or_create_return_value_symbol(), goto_program, irept::id(), goto_programt::insert_after(), INVARIANT, irept::is_not_nil(), code_function_callt::lhs(), irept::make_nil(), to_code_function_call(), to_code_type(), to_symbol_expr(), and exprt::type().
Referenced by operator()().
|
protected |
Definition at line 62 of file remove_returns.cpp.
References symbol_table_baset::add(), symbolt::base_name, id2string(), symbolt::is_static_lifetime, symbol_table_baset::lookup(), symbol_table_baset::lookup_ref(), symbolt::mode, symbolt::module, symbolt::name, code_typet::return_type(), RETURN_VALUE_SUFFIX, irept::set(), symbolt::symbol_expr(), symbol_table, to_code_type(), and symbolt::type.
Referenced by do_function_calls(), and replace_returns().
void remove_returnst::operator() | ( | goto_functionst & | goto_functions | ) |
Definition at line 220 of file remove_returns.cpp.
References do_function_calls(), Forall_goto_functions, goto_functionst::function_map, INVARIANT, and replace_returns().
void remove_returnst::operator() | ( | goto_model_functiont & | model_function, |
function_is_stubt | function_is_stub | ||
) |
Definition at line 238 of file remove_returns.cpp.
References do_function_calls(), goto_model_functiont::get_function_id(), goto_model_functiont::get_goto_function(), and replace_returns().
|
protected |
turns 'return x' into an assignment to fkt::return_value
function_id | name of the function to transform |
function | function to transform |
Definition at line 96 of file remove_returns.cpp.
References Forall_goto_program_instructions, get_or_create_return_value_symbol(), symbol_table_baset::get_writeable(), goto_program, INVARIANT, exprt::op0(), symbol_table, and symbolt::type.
Referenced by operator()().
void remove_returnst::restore | ( | goto_functionst & | goto_functions | ) |
Definition at line 429 of file remove_returns.cpp.
References Forall_goto_functions, restore_returns(), and undo_function_calls().
Referenced by restore_returns().
|
protected |
turns an assignment to fkt::return_value back into 'return x'
Definition at line 315 of file remove_returns.cpp.
References symbol_table_baset::erase(), Forall_goto_program_instructions, symbol_table_baset::get_writeable(), goto_program, irept::id(), id2string(), code_assignt::lhs(), original_return_type(), remove_skip(), RETURN_VALUE_SUFFIX, code_assignt::rhs(), symbol_table, symbol_table_baset::symbols, to_code_assign(), to_symbol_expr(), and symbolt::type.
Referenced by restore().
|
protected |
turns f(...); lhs=f::return_value; into lhs=f(...)
Definition at line 368 of file remove_returns.cpp.
References Forall_goto_program_instructions, code_function_callt::function(), symbol_exprt::get_identifier(), goto_program, irept::id(), id2string(), goto_programt::instructions, INVARIANT, code_assignt::lhs(), code_function_callt::lhs(), namespacet::lookup(), code_typet::return_type(), RETURN_VALUE_SUFFIX, code_assignt::rhs(), symbol_table, to_code_assign(), to_code_function_call(), to_code_type(), to_symbol_expr(), symbolt::type, and exprt::type().
Referenced by restore().
|
protected |
Definition at line 41 of file remove_returns.cpp.
Referenced by get_or_create_return_value_symbol(), replace_returns(), restore_returns(), and undo_function_calls().