Merge pull request #2356 from peterschrammel/fix-goto-simplification

Fix if-then-else simplifications

Author: peterschrammel

jbmc/regression/jbmc/JumpSimplification/Test.class

@@ -0,0 +1,14 @@
+public class Test {
+
+    public int foo(int i) {
+      int x = 0;
+      if (i > 0) {
+        x++;
+      }
+      else
+      {
+        x--;
+      }
+      return x + 1000;
+    }
+}

jbmc/regression/jbmc/JumpSimplification/Test.java

@@ -0,0 +1,10 @@
+CORE
+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

jbmc/regression/jbmc/JumpSimplification/test.desc

@@ -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;