Merge pull request #7046 from diffblue/Bool_tests

bug when using preincrement on _Bool

Author: kroening

regression/cbmc/Bool/bool1.c

@@ -0,0 +1,35 @@
+#include <assert.h>
+
+int main()
+{
+  _Bool b1, b2, b3;
+
+  b1 = 0;
+  b1++;
+  assert(b1);
+
+  b2 = 1;
+  b2 += 10;
+  assert(b2);
+
+  b3 = b1 + b2;
+  assert(b3 == 1);
+
+  // a struct of _Bool
+  struct
+  {
+    _Bool f1, f2, f3;
+    _Bool f4 : 1, f5 : 1;
+  } s;
+
+  assert(sizeof(s) == 4);
+
+  s.f1 = 2;
+  assert(s.f1 == 1);
+
+  s.f4 = 1;
+  assert(s.f4);
+
+  *((unsigned char *)(&s.f2)) = 1;
+  assert(s.f2);
+}

regression/cbmc/Bool4/test.desc renamed to regression/cbmc/Bool/bool1.desc

@@ -1,5 +1,5 @@
 CORE
-main.c
+bool1.c
 
 ^EXIT=0$
 ^SIGNAL=0$

regression/cbmc/Bool2/main.c renamed to regression/cbmc/Bool/bool2.c

@@ -2,9 +2,10 @@
 
 _Bool nondet_bool();
 
-int main() {
-  _Bool b1=nondet_bool();
+int main()
+{
+  _Bool b1 = nondet_bool();
 
   // guaranteed to be 0 or 1
-  assert(b1==0 || b1==1);
+  assert(b1 == 0 || b1 == 1);
 }

regression/cbmc/Bool1/test.desc renamed to regression/cbmc/Bool/bool2.desc

@@ -1,5 +1,5 @@
 CORE
-main.c
+bool2.c
 
 ^EXIT=0$
 ^SIGNAL=0$

regression/cbmc/Bool3/main.c renamed to regression/cbmc/Bool/bool3.c

@@ -1,8 +1,9 @@
 #include <assert.h>
 
-int main() {
+int main()
+{
   _Bool b1;
 
   // _NOT_ guaranteed to be 0 or 1
-  assert(b1==0 || b1==1);
+  assert(b1 == 0 || b1 == 1);
 }

regression/cbmc/Bool3/test.desc renamed to regression/cbmc/Bool/bool3.desc

@@ -1,5 +1,5 @@
 CORE
-main.c
+bool3.c
 
 ^EXIT=10$
 ^SIGNAL=0$

regression/cbmc/Bool4/main.c renamed to regression/cbmc/Bool/bool4.c

@@ -1,34 +1,35 @@
 #include <assert.h>
 
-int main() {
+int main()
+{
   _Bool b1, b2;
 
-  b1=1;
+  b1 = 1;
   b1 ^= (_Bool)1;
   assert(!b1);
 
-  b1=1;
-  b2=1;
+  b1 = 1;
+  b2 = 1;
   b1 ^= b2;
   assert(!b1);
 
-  b1=1;
-  b1 ^= (1==1);
+  b1 = 1;
+  b1 ^= (1 == 1);
   assert(!b1);
 
-  b1=1;
+  b1 = 1;
   b1 ^= 2;
   assert(b1);
 
-  b1=1;
+  b1 = 1;
   b1 ^= 3;
   assert(b1);
 
-  b1=1;
+  b1 = 1;
   b1 &= 2;
   assert(!b1);
 
-  b1=0;
+  b1 = 0;
   b1 ^= 2;
-  assert(b1==1);
+  assert(b1 == 1);
 }

regression/cbmc/Bool2/test.desc renamed to regression/cbmc/Bool/bool4.desc

@@ -1,5 +1,5 @@
 CORE
-main.c
+bool4.c
 
 ^EXIT=0$
 ^SIGNAL=0$

regression/cbmc/Bool5/full-slice.desc renamed to regression/cbmc/Bool/bool5-full-slice.desc

@@ -1,5 +1,5 @@
 CORE
-main.c
+bool5.c
 --full-slice
 Generated 4 VCC\(s\), 0 remaining after simplification
 ^VERIFICATION SUCCESSFUL$