Add tests for boolean constant propagation in C

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

regression/cbmc/boolean-condition-propagation/disequals_false.desc

@@ -0,0 +1,12 @@
+CORE
+test.c
+--function disequals_false
+^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.

regression/cbmc/boolean-condition-propagation/disequals_true.desc

@@ -0,0 +1,12 @@
+CORE
+test.c
+--function disequals_true
+^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.

regression/cbmc/boolean-condition-propagation/equals_false.desc

@@ -0,0 +1,12 @@
+CORE
+test.c
+--function equals_false
+^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.

regression/cbmc/boolean-condition-propagation/equals_true.desc

@@ -0,0 +1,12 @@
+CORE
+test.c
+--function equals_true
+^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.

regression/cbmc/boolean-condition-propagation/no_comparison.desc

@@ -0,0 +1,12 @@
+CORE
+test.c
+--function no_comparison
+^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.

regression/cbmc/boolean-condition-propagation/not_disequals_false.desc

@@ -0,0 +1,12 @@
+CORE
+test.c
+--function not_disequals_false
+^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.

regression/cbmc/boolean-condition-propagation/not_disequals_true.desc

@@ -0,0 +1,12 @@
+CORE
+test.c
+--function not_disequals_false
+^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.

regression/cbmc/boolean-condition-propagation/not_equals_false.desc

@@ -0,0 +1,12 @@
+CORE
+test.c
+--function not_equals_false
+^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.

regression/cbmc/boolean-condition-propagation/not_equals_true.desc

@@ -0,0 +1,12 @@
+CORE
+test.c
+--function not_equals_true
+^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.

regression/cbmc/boolean-condition-propagation/not_no_comparison.desc

@@ -0,0 +1,12 @@
+CORE
+test.c
+--function not_no_comparison
+^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.

regression/cbmc/boolean-condition-propagation/test.c

@@ -0,0 +1,62 @@
+#include <assert.h>
+#include <stdbool.h>
+
+void no_comparison(bool my_bool)
+{
+  if(my_bool)
+    assert(my_bool == true);
+}
+
+void not_no_comparison(bool my_bool)
+{
+  if(!my_bool)
+    assert(my_bool == false);
+}
+
+void equals_true(bool my_bool)
+{
+  if(my_bool == true)
+    assert(my_bool == true);
+}
+
+void equals_false(bool my_bool)
+{
+  if(my_bool == false)
+    assert(my_bool == false);
+}
+
+void not_equals_true(bool my_bool)
+{
+  if(!(my_bool == true))
+    assert(my_bool == false);
+}
+
+void not_equals_false(bool my_bool)
+{
+  if(!(my_bool == false))
+    assert(my_bool == true);
+}
+
+void disequals_true(bool my_bool)
+{
+  if(my_bool != true)
+    assert(my_bool == false);
+}
+
+void disequals_false(bool my_bool)
+{
+  if(my_bool != false)
+    assert(my_bool == true);
+}
+
+void not_disequals_true(bool my_bool)
+{
+  if(!(my_bool != true))
+    assert(my_bool == true);
+}
+
+void not_disequals_false(bool my_bool)
+{
+  if(!(my_bool != false))
+    assert(my_bool == false);
+}