From 2b835c68a10a348753bb8b60c6bd74cdda818afd Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Sat, 9 Dec 2017 14:10:26 +0000 Subject: [PATCH] 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. --- src/goto-programs/goto_convert.cpp | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp index 96532adfa84..85ffe47a4a4 100644 --- a/src/goto-programs/goto_convert.cpp +++ b/src/goto-programs/goto_convert.cpp @@ -290,6 +290,12 @@ void goto_convertt::finish_guarded_gotos(goto_programt &dest) for(auto it=gg.ifiter, itend=gg.gotoiter; it!=itend; ++it) it->make_skip(); } + + // Must clear this, as future functions may be converted + // using the same instance of goto_convertt, typically via + // goto_convert_functions. + + guarded_gotos.clear(); } void goto_convertt::goto_convert(const codet &code, goto_programt &dest) @@ -301,6 +307,9 @@ void goto_convertt::goto_convert_rec( const codet &code, goto_programt &dest) { + // Check that guarded_gotos was cleared after any previous use of this + // converter instance: + PRECONDITION(guarded_gotos.empty()); convert(code, dest); finish_gotos(dest);