Skip to content

Commit

Permalink
Temporary fix to enable if-then-else simplifications
Browse files Browse the repository at this point in the history
Partially reverts 199d4cc, which accidentially disabled
simplifications that require incomplete instructions to
be marked GOTO.
  • Loading branch information
peterschrammel committed Jun 15, 2018
1 parent d433438 commit 4394016
Show file tree
Hide file tree
Showing 2 changed files with 5 additions and 3 deletions.
2 changes: 1 addition & 1 deletion jbmc/regression/jbmc/JumpSimplification/test.desc
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
KNOWNBUG
CORE
Test.class
--show-goto-functions --function Test.foo
activate-multi-line-match
Expand Down
6 changes: 4 additions & 2 deletions src/goto-programs/goto_convert.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -1460,8 +1460,10 @@ void goto_convertt::convert_goto(
const codet &code,
goto_programt &dest)
{
// this instruction will turn into a goto during post-processing
goto_programt::targett t=dest.add_instruction(NO_INSTRUCTION_TYPE);
// this instruction will be completed during post-processing
// it is required to mark this as GOTO in order to enable
// simplifications in generate_ifthenelse
goto_programt::targett t = dest.add_instruction(GOTO);
t->source_location=code.source_location();
t->code=code;

Expand Down

0 comments on commit 4394016

Please sign in to comment.