Skip to content

Commit 4394016

Browse files
Temporary fix to enable if-then-else simplifications
Partially reverts 199d4cc, which accidentially disabled simplifications that require incomplete instructions to be marked GOTO.
1 parent d433438 commit 4394016

File tree

2 files changed

+5
-3
lines changed

2 files changed

+5
-3
lines changed

jbmc/regression/jbmc/JumpSimplification/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
KNOWNBUG
1+
CORE
22
Test.class
33
--show-goto-functions --function Test.foo
44
activate-multi-line-match

src/goto-programs/goto_convert.cpp

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1460,8 +1460,10 @@ void goto_convertt::convert_goto(
14601460
const codet &code,
14611461
goto_programt &dest)
14621462
{
1463-
// this instruction will turn into a goto during post-processing
1464-
goto_programt::targett t=dest.add_instruction(NO_INSTRUCTION_TYPE);
1463+
// this instruction will be completed during post-processing
1464+
// it is required to mark this as GOTO in order to enable
1465+
// simplifications in generate_ifthenelse
1466+
goto_programt::targett t = dest.add_instruction(GOTO);
14651467
t->source_location=code.source_location();
14661468
t->code=code;
14671469

0 commit comments

Comments
 (0)