diff --git a/src/goto-programs/goto_program.h b/src/goto-programs/goto_program.h index b709646ed4e..7bc9f522088 100644 --- a/src/goto-programs/goto_program.h +++ b/src/goto-programs/goto_program.h @@ -573,6 +573,14 @@ class goto_programt return instructions.insert(target, instructiont()); } + /// Insertion before the instruction pointed-to by the given instruction + /// iterator `target`. + /// \return newly inserted location + targett insert_before(const_targett target, const instructiont &i) + { + return instructions.insert(target, i); + } + /// Insertion after the instruction pointed-to by the given instruction /// iterator `target`. /// \return newly inserted location @@ -581,6 +589,14 @@ class goto_programt return instructions.insert(std::next(target), instructiont()); } + /// Insertion after the instruction pointed-to by the given instruction + /// iterator `target`. + /// \return newly inserted location + targett insert_after(const_targett target, const instructiont &i) + { + return instructions.insert(std::next(target), i); + } + /// Appends the given program `p` to `*this`. `p` is destroyed. void destructive_append(goto_programt &p) { diff --git a/src/goto-programs/remove_returns.cpp b/src/goto-programs/remove_returns.cpp index debf7865dc4..869f37d01af 100644 --- a/src/goto-programs/remove_returns.cpp +++ b/src/goto-programs/remove_returns.cpp @@ -206,20 +206,19 @@ void remove_returnst::do_function_calls( rhs = side_effect_expr_nondett( function_call.lhs().type(), i_it->source_location); - goto_programt::targett t_a=goto_program.insert_after(i_it); - t_a->make_assignment(); - t_a->source_location=i_it->source_location; - t_a->code=code_assignt(function_call.lhs(), rhs); + goto_programt::targett t_a = goto_program.insert_after( + i_it, + goto_programt::make_assignment( + code_assignt(function_call.lhs(), rhs), i_it->source_location)); // fry the previous assignment function_call.lhs().make_nil(); if(!is_stub) { - goto_programt::targett t_d=goto_program.insert_after(t_a); - t_d->make_dead(); - t_d->source_location=i_it->source_location; - t_d->code = code_deadt(*return_value); + goto_program.insert_after( + t_a, + goto_programt::make_dead(*return_value, i_it->source_location)); } } }