cprover
|
Public Member Functions | |
remove_returnst (symbol_tablet &_symbol_table) | |
void | operator() (goto_functionst &goto_functions) |
void | restore (goto_functionst &goto_functions) |
Protected Member Functions | |
void | replace_returns (goto_functionst::function_mapt::iterator f_it) |
turns 'return x' into an assignment to fkt::return_value More... | |
void | do_function_calls (goto_functionst &goto_functions, 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 'return x' into an assignment to fkt::return_value More... | |
void | undo_function_calls (goto_functionst &goto_functions, goto_programt &goto_program) |
turns f(...); lhs=f::return_value; into x=f(...) More... | |
Protected Attributes | |
symbol_tablet & | symbol_table |
Definition at line 19 of file remove_returns.cpp.
|
inlineexplicit |
Definition at line 22 of file remove_returns.cpp.
|
protected |
turns x=f(...) into f(...); lhs=f::return_value;
Definition at line 117 of file remove_returns.cpp.
References Forall_goto_program_instructions, code_function_callt::function(), goto_functions_templatet< bodyT >::function_map, irept::id(), id2string(), goto_program_templatet< codeT, guardT >::insert_after(), irept::is_not_nil(), code_function_callt::lhs(), irept::make_nil(), code_typet::return_type(), RETURN_VALUE_SUFFIX, symbol_exprt::set_identifier(), to_code_function_call(), to_code_type(), to_symbol_expr(), and exprt::type().
Referenced by operator()().
void remove_returnst::operator() | ( | goto_functionst & | goto_functions | ) |
Definition at line 192 of file remove_returns.cpp.
References do_function_calls(), Forall_goto_functions, and replace_returns().
|
protected |
turns 'return x' into an assignment to fkt::return_value
Definition at line 52 of file remove_returns.cpp.
References symbol_tablet::add(), ASSIGN, symbolt::base_name, goto_program_templatet< codeT, guardT >::empty(), Forall_goto_program_instructions, id2string(), symbolt::is_static_lifetime, symbolt::mode, symbolt::module, symbolt::name, RETURN_VALUE_SUFFIX, symbol_exprt::set_identifier(), symbol_table, symbol_tablet::symbols, symbolt::type, and exprt::type().
Referenced by operator()().
void remove_returnst::restore | ( | goto_functionst & | goto_functions | ) |
Definition at line 377 of file remove_returns.cpp.
References Forall_goto_functions, restore_returns(), and undo_function_calls().
Referenced by restore_returns().
|
protected |
turns 'return x' into an assignment to fkt::return_value
Definition at line 246 of file remove_returns.cpp.
References Forall_goto_program_instructions, irept::id(), id2string(), goto_program_templatet< codeT, guardT >::instructions, code_assignt::lhs(), original_return_type(), RETURN_VALUE_SUFFIX, code_assignt::rhs(), symbol_table, symbol_tablet::symbols, to_code_assign(), to_symbol_expr(), and symbolt::type.
Referenced by restore().
|
protected |
turns f(...); lhs=f::return_value; into x=f(...)
Definition at line 319 of file remove_returns.cpp.
References Forall_goto_program_instructions, code_function_callt::function(), symbol_exprt::get_identifier(), irept::id(), id2string(), goto_program_templatet< codeT, guardT >::instructions, 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 34 of file remove_returns.cpp.
Referenced by replace_returns(), restore_returns(), and undo_function_calls().