diff --git a/src/analyses/flow_insensitive_analysis.cpp b/src/analyses/flow_insensitive_analysis.cpp index c86c2212227..593a65a8732 100644 --- a/src/analyses/flow_insensitive_analysis.cpp +++ b/src/analyses/flow_insensitive_analysis.cpp @@ -202,8 +202,8 @@ bool flow_insensitive_analysis_baset::do_function_call( goto_programt temp; goto_programt::targett r = - temp.add(goto_programt::make_return(code_returnt(side_effect_expr_nondett( - l_call->call_lhs().type(), l_call->source_location())))); + temp.add(goto_programt::make_set_return_value(side_effect_expr_nondett( + l_call->call_lhs().type(), l_call->source_location()))); r->location_number=0; goto_programt::targett t = temp.add(goto_programt::make_end_function()); diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp index ce88275457b..9ce1c1d33d1 100644 --- a/src/goto-instrument/contracts/contracts.cpp +++ b/src/goto-instrument/contracts/contracts.cpp @@ -1178,8 +1178,8 @@ void code_contractst::add_contract_check( if(code_type.return_type() != empty_typet()) { - check.add( - goto_programt::make_return(return_stmt.value(), skip->source_location())); + check.add(goto_programt::make_set_return_value( + return_stmt.value().return_value(), skip->source_location())); } // prepend the new code to dest diff --git a/src/goto-instrument/generate_function_bodies.cpp b/src/goto-instrument/generate_function_bodies.cpp index d7deef679c1..2955a2e8232 100644 --- a/src/goto-instrument/generate_function_bodies.cpp +++ b/src/goto-instrument/generate_function_bodies.cpp @@ -357,7 +357,8 @@ class havoc_generate_function_bodiest : public generate_function_bodiest exprt return_expr = typecast_exprt::conditional_cast(aux_symbol.symbol_expr(), return_type); - add_instruction(goto_programt::make_return(code_returnt(return_expr))); + add_instruction( + goto_programt::make_set_return_value(std::move(return_expr))); add_instruction(goto_programt::make_dead(aux_symbol.symbol_expr())); } diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index 3ff25835a38..17e9ed098c8 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -1296,9 +1296,9 @@ void goto_convertt::convert_return( "function must return value", new_code.find_source_location()); - // Now add a return node to set the return value. - dest.add(goto_programt::make_return( - to_code_return(new_code), new_code.source_location())); + // Now add a 'set return value' instruction to set the return value. + dest.add(goto_programt::make_set_return_value( + new_code.return_value(), new_code.source_location())); } else { diff --git a/src/goto-programs/goto_convert_functions.cpp b/src/goto-programs/goto_convert_functions.cpp index c91b29d4c03..5048c5ae92b 100644 --- a/src/goto-programs/goto_convert_functions.cpp +++ b/src/goto-programs/goto_convert_functions.cpp @@ -138,7 +138,7 @@ void goto_convert_functionst::add_return( side_effect_expr_nondett rhs(return_type, source_location); f.body.add( - goto_programt::make_return(code_returnt(std::move(rhs)), source_location)); + goto_programt::make_set_return_value(std::move(rhs), source_location)); } void goto_convert_functionst::convert_function( diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h index 65a8a8e9800..35218ac9175 100644 --- a/src/goto-programs/goto_program.h +++ b/src/goto-programs/goto_program.h @@ -822,13 +822,22 @@ class goto_programt } } - static instructiont make_return( - code_returnt c, + static instructiont make_set_return_value( + exprt return_value, const source_locationt &l = source_locationt::nil()) { - return instructiont(std::move(c), l, SET_RETURN_VALUE, nil_exprt(), {}); + return instructiont( + code_returnt(std::move(return_value)), + l, + SET_RETURN_VALUE, + nil_exprt(), + {}); } + static instructiont make_set_return_value( + const code_returnt &code, + const source_locationt &l = source_locationt::nil()) = delete; + static instructiont make_skip(const source_locationt &l = source_locationt::nil()) { diff --git a/src/goto-programs/remove_returns.cpp b/src/goto-programs/remove_returns.cpp index 5d9a4fc5185..44d156ed857 100644 --- a/src/goto-programs/remove_returns.cpp +++ b/src/goto-programs/remove_returns.cpp @@ -314,8 +314,8 @@ bool remove_returnst::restore_returns( // replace "fkt#return_value=x;" by "return x;" const exprt rhs = instruction.assign_rhs(); - instruction = goto_programt::make_return( - code_returnt(rhs), instruction.source_location()); + instruction = goto_programt::make_set_return_value( + rhs, instruction.source_location()); did_something = true; } }