Skip to content

Commit 2b835c6

Browse files
committed
Ensure guarded_gotos is cleared after converting each function
This would previously still contain guarded GOTOs that had already been optimised by e.g. translating if(cond) GOTO 2; GOTO 1; 2: into if(!cond) GOTO 1; SKIP; 2:. This was harmless as the SKIP instructions were SKIP'd again, and the precise wording of the transformation happened to be idempotent. However, the forthcoming lazy loading patchset can remove those SKIPs between loading one function and another, and so guarded_gotos would contain dangling instruction iterators. Thus this simply avoids some wasted time and memory for now, but also enables future work.
1 parent 98017ce commit 2b835c6

File tree

1 file changed

+9
-0
lines changed

1 file changed

+9
-0
lines changed

src/goto-programs/goto_convert.cpp

+9
Original file line numberDiff line numberDiff line change
@@ -290,6 +290,12 @@ void goto_convertt::finish_guarded_gotos(goto_programt &dest)
290290
for(auto it=gg.ifiter, itend=gg.gotoiter; it!=itend; ++it)
291291
it->make_skip();
292292
}
293+
294+
// Must clear this, as future functions may be converted
295+
// using the same instance of goto_convertt, typically via
296+
// goto_convert_functions.
297+
298+
guarded_gotos.clear();
293299
}
294300

295301
void goto_convertt::goto_convert(const codet &code, goto_programt &dest)
@@ -301,6 +307,9 @@ void goto_convertt::goto_convert_rec(
301307
const codet &code,
302308
goto_programt &dest)
303309
{
310+
// Check that guarded_gotos was cleared after any previous use of this
311+
// converter instance:
312+
PRECONDITION(guarded_gotos.empty());
304313
convert(code, dest);
305314

306315
finish_gotos(dest);

0 commit comments

Comments
 (0)