Skip to content

Commit 7e976e3

Browse files
authored
Merge pull request #6407 from diffblue/set_return_value
change make_return method name and signature
2 parents cd93b5d + 4b740c2 commit 7e976e3

File tree

7 files changed

+24
-14
lines changed

7 files changed

+24
-14
lines changed

src/analyses/flow_insensitive_analysis.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -202,8 +202,8 @@ bool flow_insensitive_analysis_baset::do_function_call(
202202
goto_programt temp;
203203

204204
goto_programt::targett r =
205-
temp.add(goto_programt::make_return(code_returnt(side_effect_expr_nondett(
206-
l_call->call_lhs().type(), l_call->source_location()))));
205+
temp.add(goto_programt::make_set_return_value(side_effect_expr_nondett(
206+
l_call->call_lhs().type(), l_call->source_location())));
207207
r->location_number=0;
208208

209209
goto_programt::targett t = temp.add(goto_programt::make_end_function());

src/goto-instrument/contracts/contracts.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1178,8 +1178,8 @@ void code_contractst::add_contract_check(
11781178

11791179
if(code_type.return_type() != empty_typet())
11801180
{
1181-
check.add(
1182-
goto_programt::make_return(return_stmt.value(), skip->source_location()));
1181+
check.add(goto_programt::make_set_return_value(
1182+
return_stmt.value().return_value(), skip->source_location()));
11831183
}
11841184

11851185
// prepend the new code to dest

src/goto-instrument/generate_function_bodies.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -357,7 +357,8 @@ class havoc_generate_function_bodiest : public generate_function_bodiest
357357
exprt return_expr =
358358
typecast_exprt::conditional_cast(aux_symbol.symbol_expr(), return_type);
359359

360-
add_instruction(goto_programt::make_return(code_returnt(return_expr)));
360+
add_instruction(
361+
goto_programt::make_set_return_value(std::move(return_expr)));
361362

362363
add_instruction(goto_programt::make_dead(aux_symbol.symbol_expr()));
363364
}

src/goto-programs/goto_convert.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1296,9 +1296,9 @@ void goto_convertt::convert_return(
12961296
"function must return value",
12971297
new_code.find_source_location());
12981298

1299-
// Now add a return node to set the return value.
1300-
dest.add(goto_programt::make_return(
1301-
to_code_return(new_code), new_code.source_location()));
1299+
// Now add a 'set return value' instruction to set the return value.
1300+
dest.add(goto_programt::make_set_return_value(
1301+
new_code.return_value(), new_code.source_location()));
13021302
}
13031303
else
13041304
{

src/goto-programs/goto_convert_functions.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -138,7 +138,7 @@ void goto_convert_functionst::add_return(
138138
side_effect_expr_nondett rhs(return_type, source_location);
139139

140140
f.body.add(
141-
goto_programt::make_return(code_returnt(std::move(rhs)), source_location));
141+
goto_programt::make_set_return_value(std::move(rhs), source_location));
142142
}
143143

144144
void goto_convert_functionst::convert_function(

src/goto-programs/goto_program.h

Lines changed: 12 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -822,13 +822,22 @@ class goto_programt
822822
}
823823
}
824824

825-
static instructiont make_return(
826-
code_returnt c,
825+
static instructiont make_set_return_value(
826+
exprt return_value,
827827
const source_locationt &l = source_locationt::nil())
828828
{
829-
return instructiont(std::move(c), l, SET_RETURN_VALUE, nil_exprt(), {});
829+
return instructiont(
830+
code_returnt(std::move(return_value)),
831+
l,
832+
SET_RETURN_VALUE,
833+
nil_exprt(),
834+
{});
830835
}
831836

837+
static instructiont make_set_return_value(
838+
const code_returnt &code,
839+
const source_locationt &l = source_locationt::nil()) = delete;
840+
832841
static instructiont
833842
make_skip(const source_locationt &l = source_locationt::nil())
834843
{

src/goto-programs/remove_returns.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -314,8 +314,8 @@ bool remove_returnst::restore_returns(
314314

315315
// replace "fkt#return_value=x;" by "return x;"
316316
const exprt rhs = instruction.assign_rhs();
317-
instruction = goto_programt::make_return(
318-
code_returnt(rhs), instruction.source_location());
317+
instruction = goto_programt::make_set_return_value(
318+
rhs, instruction.source_location());
319319
did_something = true;
320320
}
321321
}

0 commit comments

Comments
 (0)