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,61 @@
+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.