Add tests for boolean constant propagation in java

Check that symex can resolve what value a boolean takes after a
condition which means that it can only take one value

Author: owen-mc-diffblue

jbmc/regression/jbmc/boolean-condition-propagation/boolean-condition-propagation-1/Test.class

@@ -0,0 +1,51 @@
+class Test {
+  static public void noComparison(boolean my_boolean) {
+    if (my_boolean)
+      assert (my_boolean == true);
+  }
+
+  static public void notNoComparison(boolean my_boolean) {
+    if (!my_boolean)
+      assert (my_boolean == false);
+  }
+
+  static public void equalsTrue(boolean my_boolean) {
+    if (my_boolean == true)
+      assert (my_boolean == true);
+  }
+
+  static public void equalsFalse(boolean my_boolean) {
+    if (my_boolean == false)
+      assert (my_boolean == false);
+  }
+
+  static public void notEqualsTrue(boolean my_boolean) {
+    if (!(my_boolean == true))
+      assert (my_boolean == false);
+  }
+
+  static public void notEqualsFalse(boolean my_boolean) {
+    if (!(my_boolean == false))
+      assert (my_boolean == true);
+  }
+
+  static public void disequalsTrue(boolean my_boolean) {
+    if (my_boolean != true)
+      assert (my_boolean == false);
+  }
+
+  static public void disequalsFalse(boolean my_boolean) {
+    if (my_boolean != false)
+      assert (my_boolean == true);
+  }
+
+  static public void notDisequalsTrue(boolean my_boolean) {
+    if (!(my_boolean != true))
+      assert (my_boolean == true);
+  }
+
+  static public void notDisequalsFalse(boolean my_boolean) {
+    if (!(my_boolean != false))
+      assert (my_boolean == false);
+  }
+};

jbmc/regression/jbmc/boolean-condition-propagation/boolean-condition-propagation-1/Test.java

@@ -0,0 +1,12 @@
+CORE
+Test.class
+--function Test.disequalsFalse
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+0 remaining after simplification$
+--
+^warning: ignoring
+--
+Assumption and GOTO condition propagation means this test should be
+entirely decided by symex.

jbmc/regression/jbmc/boolean-condition-propagation/boolean-condition-propagation-1/disequals_false.desc

@@ -0,0 +1,12 @@
+CORE
+Test.class
+--function Test.disequalsTrue
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+0 remaining after simplification$
+--
+^warning: ignoring
+--
+Assumption and GOTO condition propagation means this test should be
+entirely decided by symex.

jbmc/regression/jbmc/boolean-condition-propagation/boolean-condition-propagation-1/disequals_true.desc

@@ -0,0 +1,12 @@
+CORE
+Test.class
+--function Test.equalsFalse
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+0 remaining after simplification$
+--
+^warning: ignoring
+--
+Assumption and GOTO condition propagation means this test should be
+entirely decided by symex.

jbmc/regression/jbmc/boolean-condition-propagation/boolean-condition-propagation-1/equals_false.desc

@@ -0,0 +1,12 @@
+CORE
+Test.class
+--function Test.equalsTrue
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+0 remaining after simplification$
+--
+^warning: ignoring
+--
+Assumption and GOTO condition propagation means this test should be
+entirely decided by symex.

jbmc/regression/jbmc/boolean-condition-propagation/boolean-condition-propagation-1/equals_true.desc

@@ -0,0 +1,12 @@
+CORE
+Test.class
+--function Test.noComparison
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+0 remaining after simplification$
+--
+^warning: ignoring
+--
+Assumption and GOTO condition propagation means this test should be
+entirely decided by symex.

jbmc/regression/jbmc/boolean-condition-propagation/boolean-condition-propagation-1/no_comparison.desc

@@ -0,0 +1,12 @@
+CORE
+Test.class
+--function Test.notDisequalsFalse
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+0 remaining after simplification$
+--
+^warning: ignoring
+--
+Assumption and GOTO condition propagation means this test should be
+entirely decided by symex.

jbmc/regression/jbmc/boolean-condition-propagation/boolean-condition-propagation-1/not_disequals_false.desc

@@ -0,0 +1,12 @@
+CORE
+Test.class
+--function Test.notDisequalsFalse
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+0 remaining after simplification$
+--
+^warning: ignoring
+--
+Assumption and GOTO condition propagation means this test should be
+entirely decided by symex.

jbmc/regression/jbmc/boolean-condition-propagation/boolean-condition-propagation-1/not_disequals_true.desc

@@ -0,0 +1,12 @@
+CORE
+Test.class
+--function Test.notEqualsFalse
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+0 remaining after simplification$
+--
+^warning: ignoring
+--
+Assumption and GOTO condition propagation means this test should be
+entirely decided by symex.

jbmc/regression/jbmc/boolean-condition-propagation/boolean-condition-propagation-1/not_equals_false.desc

@@ -0,0 +1,12 @@
+CORE
+Test.class
+--function Test.notEqualsTrue
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+0 remaining after simplification$
+--
+^warning: ignoring
+--
+Assumption and GOTO condition propagation means this test should be
+entirely decided by symex.

jbmc/regression/jbmc/boolean-condition-propagation/boolean-condition-propagation-1/not_equals_true.desc

@@ -0,0 +1,12 @@
+CORE
+Test.class
+--function Test.notNoComparison
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+0 remaining after simplification$
+--
+^warning: ignoring
+--
+Assumption and GOTO condition propagation means this test should be
+entirely decided by symex.