Test for if-then-else optimisation in goto convert

The optimisation has been inadvertently broken by 199d4cc due to lack of a regression test.
NathanJPhillips · Jun 15, 2018 · d433438 · d433438
1 parent 8e6244c
commit d433438
Show file tree

Hide file tree

Showing 3 changed files with 24 additions and 0 deletions.
diff --git a/jbmc/regression/jbmc/JumpSimplification/Test.class b/jbmc/regression/jbmc/JumpSimplification/Test.class
diff --git a/jbmc/regression/jbmc/JumpSimplification/Test.java 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
@@ -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