Merge pull request #8212 from tautschnig/bugfixes/unsigned-char

Make tests pass when char is unsigned

Author: kroening

regression/cbmc-cpp/Pointer_Conversion2/main.cpp

@@ -1,5 +1,5 @@
 #include <cassert>
-char a[100];
+signed char a[100];
 
 void f(const signed char x[])
 {

regression/cbmc/pragma_cprover_enable_all/test.desc

@@ -8,7 +8,7 @@ main.c
 ^\[main\.division-by-zero\.\d+\] line 84 division by zero in x / den: FAILURE
 ^\[main\.overflow\.\d+\] line 84 arithmetic overflow on floating-point division in x / den: FAILURE
 ^\[main\.enum-range-check\.\d+\] line 85 enum range check in \(ABC\)10: FAILURE
-^\[main\.overflow\.\d+\] line 86 arithmetic overflow on signed type conversion in \(char\)\(\(signed int\)i \+ 1\): FAILURE
+^\[main\.overflow\.\d+\] line 86 arithmetic overflow on signed (to unsigned )?type conversion in \(char\)\(\(signed int\)i \+ 1\): FAILURE
 ^\[main\.overflow\.\d+\] line 87 arithmetic overflow on signed \+ in j \+ 1: FAILURE
 ^VERIFICATION FAILED$
 ^EXIT=10$