Skip to content

change make_return method name and signature #6407

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 1 commit into from
Oct 21, 2021
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 2 additions & 2 deletions src/analyses/flow_insensitive_analysis.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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());
Expand Down
4 changes: 2 additions & 2 deletions src/goto-instrument/contracts/contracts.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
3 changes: 2 additions & 1 deletion src/goto-instrument/generate_function_bodies.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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()));
}
Expand Down
6 changes: 3 additions & 3 deletions src/goto-programs/goto_convert.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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
{
Expand Down
2 changes: 1 addition & 1 deletion src/goto-programs/goto_convert_functions.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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(
Expand Down
15 changes: 12 additions & 3 deletions src/goto-programs/goto_program.h
Original file line number Diff line number Diff line change
Expand Up @@ -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())
{
Expand Down
4 changes: 2 additions & 2 deletions src/goto-programs/remove_returns.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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;
}
}
Expand Down