From d433438107146195789647f5e0529fa8036c27ab Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Fri, 15 Jun 2018 22:05:50 +0530
Subject: [PATCH 1/2] Test for if-then-else optimisation in goto convert

The optimisation has been inadvertently broken by 199d4cc
due to lack of a regression test.
---
 .../regression/jbmc/JumpSimplification/Test.class | Bin 0 -> 299 bytes
 jbmc/regression/jbmc/JumpSimplification/Test.java |  14 ++++++++++++++
 jbmc/regression/jbmc/JumpSimplification/test.desc |  10 ++++++++++
 3 files changed, 24 insertions(+)
 create mode 100644 jbmc/regression/jbmc/JumpSimplification/Test.class
 create mode 100644 jbmc/regression/jbmc/JumpSimplification/Test.java
 create mode 100644 jbmc/regression/jbmc/JumpSimplification/test.desc

diff --git a/jbmc/regression/jbmc/JumpSimplification/Test.class b/jbmc/regression/jbmc/JumpSimplification/Test.class
new file mode 100644
index 0000000000000000000000000000000000000000..c28241884103d93225000ddfe1d4ddd4d900326d
GIT binary patch
literal 299
zcmXX=J5Iwu6r8skud#7(D4+ofx`cu>lt6=o6vU@UM9tbP$RXG$IGiBoprxUqLZaXR
zoP<LlVAjg6H1l?5-rM)}`|$~251kkq?GP&=Qi0ho%A!6L=x*;)&^oHFogh6eN_RfH
z&)jrmvk4V_Q&qIPgWf>U9@aL$JF^c9Gagp6Y3_~-pNvNCvECiqC!3&!fK6TybiCA`
z*z&f2k&RtmV;hRA_@lrW0;1t-i!9_|=N<CKLJ$&7BYJBI5z$9a79-a5!NxP9xsn%{
mx%%5&)!$dI45+4cowLCo6xr}5h><o3`sxRX_!X9$hU6bTLN12@

literal 0
HcmV?d00001

diff --git a/jbmc/regression/jbmc/JumpSimplification/Test.java b/jbmc/regression/jbmc/JumpSimplification/Test.java
new file mode 100644
index 00000000000..85b3035f96c
--- /dev/null
+++ b/jbmc/regression/jbmc/JumpSimplification/Test.java
@@ -0,0 +1,14 @@
+public class Test {
+
+    public int foo(int i) {
+      int x = 0;
+      if (i > 0) {
+        x++;
+      }
+      else
+      {
+        x--;
+      }
+      return x + 1000;
+    }
+}
diff --git a/jbmc/regression/jbmc/JumpSimplification/test.desc b/jbmc/regression/jbmc/JumpSimplification/test.desc
new file mode 100644
index 00000000000..4a6517206b2
--- /dev/null
+++ b/jbmc/regression/jbmc/JumpSimplification/test.desc
@@ -0,0 +1,10 @@
+KNOWNBUG
+Test.class
+--show-goto-functions --function Test.foo
+activate-multi-line-match
+EXIT=0
+SIGNAL=0
+IF \w* <= 0 THEN GOTO 1\n\s*//.*\n\s*//.*\n\s*\w*::
+--
+IF !\(\w* <= 0\) THEN GOTO 1\n\s*//.*\n.*GOTO 2\n\s*//.*\n\s*//.*\n\s*1: \w*::
+^warning: ignoring

From 43940164eeaecbf347dd026edde488aec099cf1d Mon Sep 17 00:00:00 2001
From: Peter Schrammel <peter.schrammel@diffblue.com>
Date: Fri, 15 Jun 2018 22:14:01 +0530
Subject: [PATCH 2/2] Temporary fix to enable if-then-else simplifications

Partially reverts 199d4cc, which accidentially disabled
simplifications that require incomplete instructions to
be marked GOTO.
---
 jbmc/regression/jbmc/JumpSimplification/test.desc | 2 +-
 src/goto-programs/goto_convert.cpp                | 6 ++++--
 2 files changed, 5 insertions(+), 3 deletions(-)

diff --git a/jbmc/regression/jbmc/JumpSimplification/test.desc b/jbmc/regression/jbmc/JumpSimplification/test.desc
index 4a6517206b2..3f7c1243237 100644
--- a/jbmc/regression/jbmc/JumpSimplification/test.desc
+++ b/jbmc/regression/jbmc/JumpSimplification/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 Test.class
 --show-goto-functions --function Test.foo
 activate-multi-line-match
diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp
index 298f61aefb5..9833cc07775 100644
--- a/src/goto-programs/goto_convert.cpp
+++ b/src/goto-programs/goto_convert.cpp
@@ -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;