diff --git a/src/goto-programs/mm_io.cpp b/src/goto-programs/mm_io.cpp index 61caabd7a39..919014a8faf 100644 --- a/src/goto-programs/mm_io.cpp +++ b/src/goto-programs/mm_io.cpp @@ -56,8 +56,7 @@ void mm_io( const code_typet &ct=to_code_type(mm_io_r.type()); irep_idt identifier=to_symbol_expr(mm_io_r).get_identifier(); - irep_idt r_identifier = return_value_identifier(identifier, ns); - symbol_exprt return_value(r_identifier, ct.return_type()); + auto return_value = return_value_symbol(identifier, ns); if_exprt if_expr(integer_address(d.pointer()), return_value, d); if(!replace_expr(d, if_expr, a.rhs())) it->set_assign(a); diff --git a/src/goto-programs/remove_returns.cpp b/src/goto-programs/remove_returns.cpp index b9a395b3825..d77b140cc03 100644 --- a/src/goto-programs/remove_returns.cpp +++ b/src/goto-programs/remove_returns.cpp @@ -64,10 +64,10 @@ optionalt remove_returnst::get_or_create_return_value_symbol(const irep_idt &function_id) { const namespacet ns(symbol_table); - const irep_idt symbol_name = return_value_identifier(function_id, ns); - const symbolt *existing_symbol = symbol_table.lookup(symbol_name); - if(existing_symbol != nullptr) - return existing_symbol->symbol_expr(); + const auto symbol_expr = return_value_symbol(function_id, ns); + const auto symbol_name = symbol_expr.get_identifier(); + if(symbol_table.has_symbol(symbol_name)) + return symbol_expr; const symbolt &function_symbol = symbol_table.lookup_ref(function_id); const typet &return_type = to_code_type(function_symbol.type).return_type(); @@ -296,7 +296,8 @@ bool remove_returnst::restore_returns( // do we have X#return_value? const namespacet ns(symbol_table); - auto rv_name = return_value_identifier(function_id, ns); + auto rv_symbol = return_value_symbol(function_id, ns); + auto rv_name = rv_symbol.get_identifier(); symbol_tablet::symbolst::const_iterator rv_it= symbol_table.symbols.find(rv_name); @@ -368,12 +369,8 @@ void remove_returnst::undo_function_calls( const code_assignt &assign = next->get_assign(); - if(assign.rhs().id()!=ID_symbol) - continue; - - irep_idt rv_name = return_value_identifier(function_id, ns); - const symbol_exprt &rhs=to_symbol_expr(assign.rhs()); - if(rhs.get_identifier()!=rv_name) + const auto rv_symbol = return_value_symbol(function_id, ns); + if(assign.rhs() != rv_symbol) continue; // restore the previous assignment @@ -414,7 +411,10 @@ void restore_returns(goto_modelt &goto_model) rr.restore(goto_model.goto_functions); } -irep_idt return_value_identifier(const irep_idt &identifier, const namespacet &) +symbol_exprt +return_value_symbol(const irep_idt &identifier, const namespacet &ns) { - return id2string(identifier) + RETURN_VALUE_SUFFIX; + const symbolt &function_symbol = ns.lookup(identifier); + const typet &return_type = to_code_type(function_symbol.type).return_type(); + return symbol_exprt(id2string(identifier) + RETURN_VALUE_SUFFIX, return_type); } diff --git a/src/goto-programs/remove_returns.h b/src/goto-programs/remove_returns.h index a2af456adb5..c47d129337d 100644 --- a/src/goto-programs/remove_returns.h +++ b/src/goto-programs/remove_returns.h @@ -78,8 +78,9 @@ Date: September 2009 class goto_functionst; class goto_model_functiont; class goto_modelt; -class symbol_table_baset; class namespacet; +class symbol_table_baset; +class symbol_exprt; void remove_returns(symbol_table_baset &, goto_functionst &); @@ -94,8 +95,8 @@ void restore_returns(symbol_table_baset &, goto_functionst &); void restore_returns(goto_modelt &); -/// produces the identifier that is used to store the return +/// produces the symbol that is used to store the return /// value of the function with the given identifier -irep_idt return_value_identifier(const irep_idt &, const namespacet &); +symbol_exprt return_value_symbol(const irep_idt &, const namespacet &); #endif // CPROVER_GOTO_PROGRAMS_REMOVE_RETURNS_H diff --git a/src/goto-programs/replace_calls.cpp b/src/goto-programs/replace_calls.cpp index 9bec885e97d..bcda1f462e9 100644 --- a/src/goto-programs/replace_calls.cpp +++ b/src/goto-programs/replace_calls.cpp @@ -97,16 +97,18 @@ void replace_callst::operator()( PRECONDITION(base_type_eq(f_it1->second.type, f_it2->second.type, ns)); // check that returns have not been removed - goto_programt::const_targett next_it = std::next(it); - if(next_it != goto_program.instructions.end() && next_it->is_assign()) + if(to_code_type(f_it1->second.type).return_type().id() != ID_empty) { - const code_assignt &ca = next_it->get_assign(); - const exprt &rhs = ca.rhs(); - - INVARIANT( - rhs.id() != ID_symbol || to_symbol_expr(rhs).get_identifier() != - return_value_identifier(id, ns), - "returns must not be removed before replacing calls"); + goto_programt::const_targett next_it = std::next(it); + if(next_it != goto_program.instructions.end() && next_it->is_assign()) + { + const code_assignt &ca = next_it->get_assign(); + const exprt &rhs = ca.rhs(); + + INVARIANT( + rhs != return_value_symbol(id, ns), + "returns must not be removed before replacing calls"); + } } // Finally modify the call