consolidate integer overflow tests in one directory

This moves the tests that relate to integer overflow checking into one directory.

Author: kroening

regression/cbmc/Overflow_Multiplication1/falsealarm.c

@@ -1,5 +1,5 @@
 CORE
-main.c
+leftshift_overflow.c
 --signed-overflow-check --c89
 ^EXIT=10$
 ^SIGNAL=0$

regression/cbmc/Overflow_Leftshift1/test-c89.desc renamed to regression/cbmc/overflow/leftshift_overflow-c89.desc

@@ -1,5 +1,5 @@
 CORE
-main.c
+leftshift_overflow.c
 --signed-overflow-check --c99
 ^EXIT=10$
 ^SIGNAL=0$

regression/cbmc/Overflow_Leftshift1/test-c99.desc renamed to regression/cbmc/overflow/leftshift_overflow-c99.desc

@@ -8,10 +8,10 @@ int main()
   unsigned r = x << ((sizeof(unsigned) - 1) * 8 + 1);
 
   // signed, owing to promotion, and cannot overflow
-  r=x << ((sizeof(unsigned)-1)*8-1);
+  r = x << ((sizeof(unsigned) - 1) * 8 - 1);
 
   // unsigned
-  r=(unsigned)x << ((sizeof(unsigned)-1)*8);
+  r = (unsigned)x << ((sizeof(unsigned) - 1) * 8);
 
   // negative value or zero, not an overflow
   int s = -x << ((sizeof(int) - 1) * 8);

regression/cbmc/Overflow_Leftshift1/main.c renamed to regression/cbmc/overflow/leftshift_overflow.c

@@ -1,7 +1,8 @@
-int main() {
+int main()
+{
   signed int i, j;
 
-  i=j;
+  i = j;
 
   i++;
 }

regression/cbmc/Overflow_Addition1/main.c renamed to regression/cbmc/overflow/signed_addition_overflow1.c

@@ -1,5 +1,5 @@
 CORE
-main.c
+signed_addition_overflow1.c
 --signed-overflow-check
 ^EXIT=10$
 ^SIGNAL=0$

regression/cbmc/Overflow_Addition1/test.desc renamed to regression/cbmc/overflow/signed_addition_overflow1.desc

@@ -1,5 +1,5 @@
 CORE
-main.c
+signed_addition_overflow2.c
 --signed-overflow-check
 ^EXIT=10$
 ^SIGNAL=0$

regression/cbmc/Overflow_Addition2/main.c renamed to regression/cbmc/overflow/signed_addition_overflow2.c

@@ -1,5 +1,5 @@
 CORE
-main.c
+signed_addition_overflow3.c
 --signed-overflow-check --conversion-check
 ^EXIT=10$
 ^SIGNAL=0$

regression/cbmc/Overflow_Addition2/test.desc renamed to regression/cbmc/overflow/signed_addition_overflow2.desc

@@ -1,5 +1,5 @@
 CORE
-main.c
+signed_addition_overflow4.c
 --signed-overflow-check --conversion-check
 ^EXIT=10$
 ^SIGNAL=0$

regression/cbmc/Overflow_Addition3/main.c renamed to regression/cbmc/overflow/signed_addition_overflow3.c

@@ -0,0 +1,16 @@
+// From Cousot's FMSD paper
+
+void main()
+{
+  int x, y, _x, _y;
+
+  x = _x;
+  y = _y;
+
+  if(
+    (-4681 < y) && (y < 4681) && (x < 32767) && (-32767 < x) &&
+    ((7 * y * y - 1) == x * x))
+  {
+    y = 1 / x;
+  }
+}

regression/cbmc/Overflow_Addition3/test.desc renamed to regression/cbmc/overflow/signed_addition_overflow3.desc

@@ -1,5 +1,5 @@
 CORE
-main.c
+signed_multiplication1.c
 --signed-overflow-check
 ^EXIT=0$
 ^SIGNAL=0$

regression/cbmc/Overflow_Addition4/main.c renamed to regression/cbmc/overflow/signed_addition_overflow4.c

@@ -1,19 +1,19 @@
-#define INT_MIN (-1<<(sizeof(int)*8-1))
+#define INT_MIN (-1 << (sizeof(int) * 8 - 1))
 
 int main()
 {
   int a, b, neg;
 
   // this should not overflow, even not for a=INT_MIN
-  b=a-a;
+  b = a - a;
 
   // this should also not overflow as long as pos<0
-  if(neg<0)
-    b=neg-INT_MIN;
+  if(neg < 0)
+    b = neg - INT_MIN;
 
   int x, y, z;
 
-  x = INT_MIN+1;
+  x = INT_MIN + 1;
   y = INT_MIN;
-  z = x-y; // neither
+  z = x - y; // neither
 }

regression/cbmc/Overflow_Addition4/test.desc renamed to regression/cbmc/overflow/signed_addition_overflow4.desc

@@ -1,5 +1,5 @@
 CORE
-falsealarm.c
+signed_subtraction1.c
 --signed-overflow-check
 ^EXIT=0$
 ^SIGNAL=0$