Add tests for overflows

There is an interaction between type promotion and
overflow detection. In the case of compound assignments
type promotion is broken.

Author: peterschrammel

regression/cbmc/Overflow_Addition2/main.c

@@ -0,0 +1,6 @@
+void main()
+{
+  signed char i, j;
+  i = j;
+  i += 1;
+}

regression/cbmc/Overflow_Addition2/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--signed-overflow-check
+^EXIT=10$
+^SIGNAL=0$
+^\[.*\] .* arithmetic overflow on signed \+ in .*: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring

regression/cbmc/Overflow_Addition3/main.c

@@ -0,0 +1,6 @@
+void main()
+{
+  signed char i, j;
+  i = j;
+  i += 1;
+}

regression/cbmc/Overflow_Addition3/test.desc

@@ -0,0 +1,15 @@
+KNOWNBUG
+main.c
+--signed-overflow-check --conversion-check
+^EXIT=10$
+^SIGNAL=0$
+^\[.*\] .* arithmetic overflow on signed \+ in .*: SUCCESS
+^\[.*\] .* arithmetic overflow on signed type conversion in .*: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+--
+The addition is done in signed int; hence, the overflow is only detected
+on conversion.
+
+See #4208.

regression/cbmc/Overflow_Addition4/main.c

@@ -0,0 +1,6 @@
+void main()
+{
+  signed char i, j;
+  i = j;
+  i = i + 1;
+}

regression/cbmc/Overflow_Addition4/test.desc

@@ -0,0 +1,13 @@
+CORE
+main.c
+--signed-overflow-check --conversion-check
+^EXIT=10$
+^SIGNAL=0$
+^\[.*\] .* arithmetic overflow on signed \+ in .*: SUCCESS
+^\[.*\] .* arithmetic overflow on signed type conversion in .*: FAILURE$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+--
+The addition is done in signed int; hence, the overflow is only detected
+on conversion.