Tests: use types that are smaller than long on all platforms

Some tests assumed that sizeof(int) < sizeof(long), which need not be
the case.

Author: tautschnig

regression/cbmc/array_of_bool_as_bitvec/main.c

@@ -11,7 +11,7 @@ void main()
   __CPROVER_bool y[8] = {false};
   bool *z = calloc(8, sizeof(bool));
 
-  unsigned idx;
+  unsigned char idx;
   __CPROVER_assume(0 <= idx && idx < 8);
 
   assert(w[idx] == x[idx]);

regression/cbmc/array_of_bool_as_bitvec/test-smt2-outfile.desc

@@ -2,14 +2,14 @@ CORE broken-smt-backend
 main.c
 --smt2 --outfile -
 \(= \(select array_of\.0 i\) \(ite false #b1 #b0\)\)
-\(= \(select array\.1 \(\(_ zero_extend 32\) \|main::1::idx!0@1#1\|\)\) #b1\)
-\(= \(select array\.1 \(_ bv\d+ 64\)\) \(ite false #b1 #b0\)\)
+\(= \(select array\.1 \(\(_ zero_extend \d+\) \|main::1::idx!0@1#1\|\)\) #b1\)
+\(= \(select array\.1 \(_ bv\d+ \d+\)\) \(ite false #b1 #b0\)\)
 ^EXIT=0$
 ^SIGNAL=0$
 --
 \(= \(select array_of\.0 i\) false\)
-\(= \(select array\.1 \(\(_ zero_extend 32\) \|main::1::idx!0@1#1\|\)\) #b1 #b0\)
-\(= \(select array\.1 \(_ bv\d+ 64\)\) false\)
+\(= \(select array\.1 \(\(_ zero_extend \d+\) \|main::1::idx!0@1#1\|\)\) #b1 #b0\)
+\(= \(select array\.1 \(_ bv\d+ \d+\)\) false\)
 --
 This test checks for correctness of BitVec-array encoding of Boolean arrays.
 

regression/cbmc/ptr_arithmetic_on_null/main.c

@@ -5,7 +5,7 @@ void main()
   assert(NULL != (NULL + 1));
   assert(NULL != (NULL - 1));
 
-  int offset;
+  signed char offset;
   __CPROVER_assume(offset != 0);
   assert(NULL != (NULL + offset));
 

regression/cbmc/ptr_arithmetic_on_null/test.desc

@@ -3,7 +3,7 @@ main.c
 
 ^\[main.assertion.1\] line .* assertion \(\(char \*\)NULL\) != \(char \*\)\(void \*\)0 \+ (\(.*\))?1: SUCCESS$
 ^\[main.assertion.2\] line .* assertion \(\(char \*\)NULL\) != \(char \*\)\(void \*\)0 - (\(.*\))?1: SUCCESS$
-^\[main.assertion.3\] line .* assertion \(\(char \*\)NULL\) != \(char \*\)\(void \*\)0 \+ (\(.*\))?offset: SUCCESS$
+^\[main.assertion.3\] line .* assertion \(\(char \*\)NULL\) != \(char \*\)\(void \*\)0 \+ \(.*\)offset: SUCCESS$
 ^\[main.assertion.4\] line .* assertion \(char \*\)\(void \*\)0 - \(char \*\)\(void \*\)0 == (\(.*\))?0: SUCCESS$
 ^\[main.assertion.5\] line .* assertion ptr - \(signed int \*\)\(void \*\)0 == (\(.*\))?0: FAILURE$
 ^\[main.assertion.6\] line .* assertion \(ptr - (\(.*\))?1\) \+ (\(.*\))?1 == \(\(.* \*\)NULL\): SUCCESS$