improve test for signed left-shift overflows

Author: Daniel Kroening

regression/cbmc/Overflow_Leftshift1/main.c

@@ -1,11 +1,21 @@
 int main()
 {
   unsigned char x;
+
+  // signed, owing to promotion, and may overflow
   unsigned r=x << ((sizeof(unsigned)-1)*8);
+
+  // signed, owing to promotion, and cannot overflow
   r=x << ((sizeof(unsigned)-1)*8-1);
+
+  // unsigned
   r=(unsigned)x << ((sizeof(unsigned)-1)*8);
 
-  int s=-1 << ((sizeof(int)-1)*8);
-  s=-256 << ((sizeof(int)-1)*8);
+  // negative value or zero, not an overflow
+  int s = -x << ((sizeof(int) - 1) * 8);
+
+  // overflow
+  s = 1 << x;
+
   return 0;
 }

regression/cbmc/Overflow_Leftshift1/test.desc

@@ -3,8 +3,13 @@ main.c
 --signed-overflow-check
 ^EXIT=10$
 ^SIGNAL=0$
-^\[.*\] .* arithmetic overflow on signed shl in .*: FAILURE$
-^\*\* 2 of 4 failed
+^\[.*\] line 6 arithmetic overflow on signed shl in .*: FAILURE$
+^\[.*\] line 9 arithmetic overflow on signed shl in .*: SUCCESS$
+^\[.*\] line 15 arithmetic overflow on signed shl in .*: SUCCESS$
+^\[.*\] line 18 arithmetic overflow on signed shl in .*: FAILURE$
+^\*\* 2 of 5 failed
 ^VERIFICATION FAILED$
 --
 ^warning: ignoring
+^\[.*\] line 12 arithmetic overflow on signed shl in .*: .*
+^\[.*\] line 21 arithmetic overflow on signed shl in .*: .*