Skip to content

Commit 768a2c7

Browse files
committed
remove unusuable goto_programt::make_return variant
The instruction generated by this variant violates an invariant, and thus, this method is not usable.
1 parent 61fd24d commit 768a2c7

File tree

3 files changed

+4
-9
lines changed

3 files changed

+4
-9
lines changed

src/goto-programs/goto_program.h

Lines changed: 0 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -845,12 +845,6 @@ class goto_programt
845845
}
846846
}
847847

848-
static instructiont
849-
make_return(const source_locationt &l = source_locationt::nil())
850-
{
851-
return instructiont(code_returnt(), l, SET_RETURN_VALUE, nil_exprt(), {});
852-
}
853-
854848
static instructiont make_return(
855849
code_returnt c,
856850
const source_locationt &l = source_locationt::nil())

unit/goto-instrument/cover_instrument.cpp

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@ TEST_CASE("cover_intrument_end_of_function", "[core]")
1717
goto_programt::make_function_call(code_function_callt({}, {})));
1818
goto_program.add(
1919
goto_programt::make_function_call(code_function_callt({}, {})));
20-
goto_program.add(goto_programt::make_return());
20+
goto_program.add(goto_programt::make_end_function());
2121
// Act
2222
cover_instrument_end_of_function(
2323
"foo", goto_program, goto_programt::make_assertion);
@@ -37,7 +37,7 @@ TEST_CASE("cover_instrument_end_of_function with custom expression", "[core]")
3737
goto_programt::make_function_call(code_function_callt({}, {})));
3838
goto_program.add(
3939
goto_programt::make_function_call(code_function_callt({}, {})));
40-
goto_program.add(goto_programt::make_return());
40+
goto_program.add(goto_programt::make_end_function());
4141
const cover_instrumenter_baset::assertion_factoryt assertion_factory =
4242
[](const exprt &, const source_locationt &location) {
4343
return goto_programt::make_assertion(true_exprt{}, location);

unit/goto-programs/goto_program_validate.cpp

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -197,7 +197,8 @@ SCENARIO("Validation of a goto program", "[core][goto-programs][validate]")
197197
auto &function_map = goto_model.goto_functions.function_map;
198198
auto it = function_map.find("g");
199199
auto &instructions = it->second.body.instructions;
200-
instructions.insert(instructions.begin(), goto_programt::make_return());
200+
instructions.insert(
201+
instructions.begin(), goto_programt::make_return(code_returnt()));
201202

202203
goto_model_validation_optionst validation_options{
203204
goto_model_validation_optionst ::set_optionst::all_false};

0 commit comments

Comments
 (0)