Skip to content

Commit ef5d2ad

Browse files
committed
Use const_cast_target instead of local get_mutable
1 parent d5b5aee commit ef5d2ad

File tree

2 files changed

+3
-9
lines changed

2 files changed

+3
-9
lines changed

src/goto-instrument/unwind.cpp

+3-2
Original file line numberDiff line numberDiff line change
@@ -244,7 +244,7 @@ void goto_unwindt::unwind(
244244
goto_programt::targett t_goto=goto_program.insert_before(loop_exit);
245245
unwind_log.insert(t_goto, loop_exit->location_number);
246246

247-
t_goto->make_goto(get_mutable(goto_program, loop_exit));
247+
t_goto->make_goto(goto_program.const_cast_target(loop_exit));
248248
t_goto->source_location=loop_exit->source_location;
249249
t_goto->function=loop_exit->function;
250250
t_goto->guard=true_exprt();
@@ -269,7 +269,8 @@ void goto_unwindt::unwind(
269269

270270
// re-direct any branches that go to loop_head to loop_iter
271271

272-
for(goto_programt::targett t=get_mutable(goto_program, loop_head);
272+
for(goto_programt::targett
273+
t=goto_program.const_cast_target(loop_head);
273274
t!=loop_iter; t++)
274275
{
275276
if(!t->is_goto())

src/goto-instrument/unwind.h

-7
Original file line numberDiff line numberDiff line change
@@ -117,13 +117,6 @@ class goto_unwindt
117117
const goto_programt::const_targett start,
118118
const goto_programt::const_targett end, // exclusive
119119
goto_programt &goto_program); // result
120-
121-
goto_programt::targett get_mutable(
122-
goto_programt &goto_program,
123-
const goto_programt::const_targett t) const
124-
{
125-
return goto_program.instructions.erase(t, t);
126-
}
127120
};
128121

129122
#endif // CPROVER_GOTO_INSTRUMENT_UNWIND_H

0 commit comments

Comments
 (0)