Test 32-bit builds in CI and fix platform-specific code and tests

.github/workflows/pull-request-checks.yaml

@@ -442,6 +442,52 @@ jobs:
       - name: Run tests
         run: cd build; ctest . -V -L CORE -j2
 
+  # This job takes approximately 30 to 60 minutes
+  check-ubuntu-22_04-cmake-gcc-32bit:
+    runs-on: ubuntu-22.04
+    steps:
+      - uses: actions/checkout@v3
+        with:
+          submodules: recursive
+      - name: Fetch dependencies
+        env:
+          # This is needed in addition to -yq to prevent apt-get from asking for
+          # user input
+          DEBIAN_FRONTEND: noninteractive
+        run: |
+          sudo apt-get update
+          sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc gdb g++ maven flex bison libxml2-utils ccache doxygen z3 g++-multilib
+      - name: Confirm z3 solver is available and log the version installed
+        run: z3 --version
+      - name: Download cvc-5 from the releases page and make sure it can be deployed
+        run: |
+          wget -O cvc5 https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux
+          chmod u+x cvc5
+          mv cvc5 /usr/local/bin
+          cvc5 --version
+      - name: Prepare ccache
+        uses: actions/cache@v3
+        with:
+          path: .ccache
+          key: ${{ runner.os }}-22.04-Release-32-${{ github.ref }}-${{ github.sha }}-PR
+          restore-keys: |
+            ${{ runner.os }}-22.04-Release-32-${{ github.ref }}
+            ${{ runner.os }}-22.04-Release-32
+      - name: ccache environment
+        run: |
+          echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
+          echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
+      - name: Configure using CMake
+        run: cmake -S . -Bbuild -G Ninja -DCMAKE_BUILD_TYPE=Release -DCMAKE_C_COMPILER=/usr/bin/gcc -DCMAKE_CXX_COMPILER=/usr/bin/g++ -Dsat_impl="minisat2;cadical" -DCMAKE_CXX_FLAGS=-m32
+      - name: Zero ccache stats and limit in size
+        run: ccache -z --max-size=500M
+      - name: Build with Ninja
+        run: ninja -C build -j2
+      - name: Print ccache stats
+        run: ccache -s
+      - name: Run tests
+        run: cd build; ctest . -V -L CORE -j2
+
   # This job takes approximately 5 to 24 minutes
   check-ubuntu-20_04-cmake-gcc-KNOWNBUG:
     runs-on: ubuntu-20.04

regression/cbmc-incr-smt2/arrays_traces/array_write.desc

@@ -3,7 +3,7 @@ array_write.c
 --trace
 Passing problem to incremental SMT2 solving
 ^Trace for main\.assertion\.2
-example_array\[\d{1,4}ll?\]=42
+example_array\[\d{1,4}l?l?\]=42
 ^EXIT=10$
 ^SIGNAL=0$
 --

regression/cbmc-incr-smt2/enums/enum_in_array.desc

@@ -4,9 +4,9 @@ enum_in_array.c
 Passing problem to incremental SMT2 solving
 line 18 Array at index 0 is V0, so this should fail: FAILURE
 i=0u \(00000000 00000000 00000000 00000000\)
-e\[0l+\]=/\*enum\*/V0 \(00000000 00000000 00000000 00000000\)
-e\[1l+\]=/\*enum\*/V1 \(00000000 00000000 00000000 00000001\)
-e\[2l+\]=/\*enum\*/V2 \(00000000 00000000 00000000 00000010\)
+e\[0l*\]=/\*enum\*/V0 \(00000000 00000000 00000000 00000000\)
+e\[1l*\]=/\*enum\*/V1 \(00000000 00000000 00000000 00000001\)
+e\[2l*\]=/\*enum\*/V2 \(00000000 00000000 00000000 00000010\)
 ^EXIT=10$
 ^SIGNAL=0$
 --

regression/cbmc-incr-smt2/nondeterministic-int-assert/stdout-match.desc

@@ -4,13 +4,13 @@ test.c
 Starting Bounded Model Checking
 ^\(set-option :produce-models true\)$
 ^\(set-logic ALL\)$
-^\(declare-fun size_of_object \(\(_ BitVec 8\)\) \(_ BitVec 64\)\)$
+^\(declare-fun size_of_object \(\(_ BitVec 8\)\) \(_ BitVec \d+\)\)$
 ^Passing problem to incremental SMT2 solving via SMT2 incremental dry-run$
 ^\(define-fun B0 \(\) Bool true\)$
 ^\(define-fun B2 \(\) Bool \(not false\)\)$
 ^\(assert B2\)$
-^\(assert \(= \(size_of_object \(_ bv1 8\)\) \(_ bv0 64\)\)\)$
-^\(assert \(= \(size_of_object \(_ bv0 8\)\) \(_ bv0 64\)\)\)$
+^\(assert \(= \(size_of_object \(_ bv1 8\)\) \(_ bv0 \d+\)\)\)$
+^\(assert \(= \(size_of_object \(_ bv0 8\)\) \(_ bv0 \d+\)\)\)$
 ^\(check-sat\)$
 ^EXIT=0$
 ^SIGNAL=0$

regression/cbmc-incr-smt2/pointers-relational-operators/pointers_assume.c

@@ -16,7 +16,6 @@ int main()
   }
 
   __CPROVER_assume(y >= z);
-  __CPROVER_assert(x != y, "x != y: expected successful");
   __CPROVER_assert(x == y, "x == y: expected failure");
 
   __CPROVER_assume(z >= x);

regression/cbmc-incr-smt2/pointers-relational-operators/pointers_assume.desc

@@ -1,11 +1,10 @@
 CORE
 pointers_assume.c
 --trace
-\[main\.assertion\.1\] line \d+ x != y: expected successful: SUCCESS
-\[main\.assertion\.2\] line \d+ x == y: expected failure: FAILURE
-\[main\.assertion\.3\] line \d+ z >= x: expected successful: SUCCESS
-\[main\.assertion\.4\] line \d+ z <= y: expected successful: SUCCESS
-\[main\.assertion\.5\] line \d+ z <= x: expected failure: FAILURE
+\[main\.assertion\.1\] line \d+ x == y: expected failure: FAILURE
+\[main\.assertion\.2\] line \d+ z >= x: expected successful: SUCCESS
+\[main\.assertion\.3\] line \d+ z <= y: expected successful: SUCCESS
+\[main\.assertion\.4\] line \d+ z <= x: expected failure: FAILURE
 ^EXIT=10$
 ^SIGNAL=0$
 --

regression/cbmc-incr-smt2/pointers/object_size.desc

@@ -5,9 +5,9 @@ line 12 Expected int sizes\.: SUCCESS
 line 13 Size is always 2\. \(Can be disproved\.\): FAILURE
 line 14 Size is always 4\. \(Can be disproved\.\): FAILURE
 line 16 Size of NULL\.: FAILURE
-size=2ul
-size=4ul
-null_size=0ul
+size=2ul*
+size=4ul*
+null_size=0ul*
 ^EXIT=10$
 ^SIGNAL=0$
 --

regression/cbmc-incr-smt2/structs/large_array_of_struct_nondet_index.desc

@@ -9,7 +9,7 @@ line 17 assertion struct_array\[x\]\.eggs \+ struct_array\[x\]\.ham != 11\: FAIL
 \{\s*\.eggs=\d+,\s*\.ham=7\s*\}
 \{\s*\.eggs=\d+,\s*\.ham=8\s*\}
 x=\d{1,4}\s
-struct_array\[\(signed (long )+int\)x\]\.eggs=3
+struct_array\[(\(signed (long )+int\))?x\]\.eggs=3
 --
 --
 This test covers support for examples with large arrays of structs using nondet

regression/cbmc-library/write-01/main.c

@@ -13,6 +13,7 @@ int main()
 
   __CPROVER_assume(fd >= 0);
   __CPROVER_assume(nbytes < SIZE);
+  __CPROVER_assume(fd <= SSIZE_MAX / sizeof(struct __CPROVER_pipet));
 
   write(fd, ptr, nbytes);
 }

regression/cbmc-primitives/exists_memory_checks/invalid_index_range.desc

@@ -5,7 +5,7 @@ invalid_index_range.c
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 \[main\.assertion\.1\] line 9 assertion __CPROVER_exists \{ int i; \(0 <= i && i < 20\) && a\[i\] == i \*i \}: SUCCESS
-line 9 dereference failure: pointer outside object bounds in a\[\(signed (long|long long) int\)i\]: FAILURE
+line 9 dereference failure: pointer outside object bounds in a\[(\(signed (long|long long) int\))?i\]: FAILURE
 --
 --
 Check that memory checks fail for pointer dereferences inside an existential

regression/cbmc-primitives/exists_memory_checks/negated_exists.desc

@@ -5,12 +5,12 @@ negated_exists.c
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 \[main\.assertion\.1\] line 9 assertion !__CPROVER_exists \{ int i; \(0 <= i && i < 10\) && a\[i\] == 42 \}: SUCCESS
-\[main\.pointer_dereference\.7\] line 9 dereference failure: pointer NULL in a\[\(signed (long|long long) int\)i\]: SUCCESS
-\[main\.pointer_dereference\.8\] line 9 dereference failure: pointer invalid in a\[\(signed (long|long long) int\)i\]: SUCCESS
-\[main\.pointer_dereference\.9\] line 9 dereference failure: deallocated dynamic object in a\[\(signed (long|long long) int\)i\]: SUCCESS
-\[main\.pointer_dereference\.10\] line 9 dereference failure: dead object in a\[\(signed (long|long long) int\)i\]: SUCCESS
-\[main\.pointer_dereference\.11\] line 9 dereference failure: pointer outside object bounds in a\[\(signed (long|long long) int\)i\]: SUCCESS
-\[main\.pointer_dereference\.12\] line 9 dereference failure: invalid integer address in a\[\(signed (long|long long) int\)i\]: SUCCESS
+\[main\.pointer_dereference\.7\] line 9 dereference failure: pointer NULL in a\[(\(signed (long|long long) int\))?i\]: SUCCESS
+\[main\.pointer_dereference\.8\] line 9 dereference failure: pointer invalid in a\[(\(signed (long|long long) int\))?i\]: SUCCESS
+\[main\.pointer_dereference\.9\] line 9 dereference failure: deallocated dynamic object in a\[(\(signed (long|long long) int\))?i\]: SUCCESS
+\[main\.pointer_dereference\.10\] line 9 dereference failure: dead object in a\[(\(signed (long|long long) int\))?i\]: SUCCESS
+\[main\.pointer_dereference\.11\] line 9 dereference failure: pointer outside object bounds in a\[(\(signed (long|long long) int\))?i\]: SUCCESS
+\[main\.pointer_dereference\.12\] line 9 dereference failure: invalid integer address in a\[(\(signed (long|long long) int\))?i\]: SUCCESS
 --
 --
 Check that memory checks pass for valid pointer dereferences inside a negated

regression/cbmc-primitives/exists_memory_checks/smt_missing_range_check.desc

@@ -5,7 +5,7 @@ smt_missing_range_check.c
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
 \[main\.assertion\.1\] line \d assertion __CPROVER_exists \{ int i; a\[i\] == i \*i \}: SUCCESS
-\[main\.pointer_dereference\.11\] line \d dereference failure: pointer outside object bounds in a\[\(signed (long|long long) int\)i\]: FAILURE
+\[main\.pointer_dereference\.11\] line \d dereference failure: pointer outside object bounds in a\[(\(signed (long|long long) int\))?i\]: FAILURE
 --
 --
 Check that memory checks fail for pointer dereferences inside an existential

regression/cbmc-primitives/exists_memory_checks/valid_index_range.desc

@@ -5,12 +5,12 @@ valid_index_range.c
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
 \[main\.assertion\.1\] line 9 assertion __CPROVER_exists \{ int i; \(0 <= i && i < 10\) && a\[i\] == i \*i \}: SUCCESS
-\[main\.pointer_dereference\.7\] line 9 dereference failure: pointer NULL in a\[\(signed (long|long long) int\)i\]: SUCCESS
-\[main\.pointer_dereference\.8\] line 9 dereference failure: pointer invalid in a\[\(signed (long|long long) int\)i\]: SUCCESS
-\[main\.pointer_dereference\.9\] line 9 dereference failure: deallocated dynamic object in a\[\(signed (long|long long) int\)i\]: SUCCESS
-\[main\.pointer_dereference\.10\] line 9 dereference failure: dead object in a\[\(signed (long|long long) int\)i\]: SUCCESS
-\[main\.pointer_dereference\.11\] line 9 dereference failure: pointer outside object bounds in a\[\(signed (long|long long) int\)i\]: SUCCESS
-\[main\.pointer_dereference\.12\] line 9 dereference failure: invalid integer address in a\[\(signed (long|long long) int\)i\]: SUCCESS
+\[main\.pointer_dereference\.7\] line 9 dereference failure: pointer NULL in a\[(\(signed (long|long long) int\))?i\]: SUCCESS
+\[main\.pointer_dereference\.8\] line 9 dereference failure: pointer invalid in a\[(\(signed (long|long long) int\))?i\]: SUCCESS
+\[main\.pointer_dereference\.9\] line 9 dereference failure: deallocated dynamic object in a\[(\(signed (long|long long) int\))?i\]: SUCCESS
+\[main\.pointer_dereference\.10\] line 9 dereference failure: dead object in a\[(\(signed (long|long long) int\))?i\]: SUCCESS
+\[main\.pointer_dereference\.11\] line 9 dereference failure: pointer outside object bounds in a\[(\(signed (long|long long) int\))?i\]: SUCCESS
+\[main\.pointer_dereference\.12\] line 9 dereference failure: invalid integer address in a\[(\(signed (long|long long) int\))?i\]: SUCCESS
 --
 --
 Check that memory checks pass for valid pointer dereferences inside an

regression/cbmc-primitives/forall_6231_1/test.desc

@@ -4,12 +4,12 @@ test.c
 ^EXIT=0$
 ^SIGNAL=0$
 \[main\.assertion\.2\] line \d+ assertion __CPROVER_forall \{ int i ; \(0 <= i && i < 1\) ==> \*\(a\+i\) == \*\(a\+i\) \}: SUCCESS
-\[main\.pointer_dereference\.7\] line \d+ dereference failure: pointer NULL in a\[\(signed (long|long long) int\)i\]: SUCCESS
-\[main\.pointer_dereference\.8\] line \d+ dereference failure: pointer invalid in a\[\(signed (long|long long) int\)i\]: SUCCESS
-\[main\.pointer_dereference\.9\] line \d+ dereference failure: deallocated dynamic object in a\[\(signed (long|long long) int\)i\]: SUCCESS
-\[main\.pointer_dereference\.10\] line \d+ dereference failure: dead object in a\[\(signed (long|long long) int\)i\]: SUCCESS
-\[main\.pointer_dereference\.11\] line \d+ dereference failure: pointer outside object bounds in a\[\(signed (long|long long) int\)i\]: SUCCESS
-\[main\.pointer_dereference\.12\] line \d+ dereference failure: invalid integer address in a\[\(signed (long|long long) int\)i\]: SUCCESS
+\[main\.pointer_dereference\.7\] line \d+ dereference failure: pointer NULL in a\[(\(signed (long|long long) int\))?i\]: SUCCESS
+\[main\.pointer_dereference\.8\] line \d+ dereference failure: pointer invalid in a\[(\(signed (long|long long) int\))?i\]: SUCCESS
+\[main\.pointer_dereference\.9\] line \d+ dereference failure: deallocated dynamic object in a\[(\(signed (long|long long) int\))?i\]: SUCCESS
+\[main\.pointer_dereference\.10\] line \d+ dereference failure: dead object in a\[(\(signed (long|long long) int\))?i\]: SUCCESS
+\[main\.pointer_dereference\.11\] line \d+ dereference failure: pointer outside object bounds in a\[(\(signed (long|long long) int\))?i\]: SUCCESS
+\[main\.pointer_dereference\.12\] line \d+ dereference failure: invalid integer address in a\[(\(signed (long|long long) int\))?i\]: SUCCESS
 ^VERIFICATION SUCCESSFUL$
 --
 --

regression/cbmc-primitives/forall_6231_2/test.desc

@@ -4,19 +4,19 @@ test.c
 ^EXIT=0$
 ^SIGNAL=0$
 \[main\.assertion\.1\] line \d+ assertion __CPROVER_forall \{ int i ; \(0 <= i && i < 1\) ==> \*\(a\+i\) == \*\(a\+i\) \}: SUCCESS
-\[main\.pointer_dereference\.1\] line \d+ dereference failure: pointer NULL in a\[\(signed (long|long long) int\)i\]: SUCCESS
-\[main\.pointer_dereference\.2\] line \d+ dereference failure: pointer invalid in a\[\(signed (long|long long) int\)i\]: SUCCESS
-\[main\.pointer_dereference\.3\] line \d+ dereference failure: deallocated dynamic object in a\[\(signed (long|long long) int\)i\]: SUCCESS
-\[main\.pointer_dereference\.4\] line \d+ dereference failure: dead object in a\[\(signed (long|long long) int\)i\]: SUCCESS
-\[main\.pointer_dereference\.5\] line \d+ dereference failure: pointer outside object bounds in a\[\(signed (long|long long) int\)i\]: SUCCESS
-\[main\.pointer_dereference\.6\] line \d+ dereference failure: invalid integer address in a\[\(signed (long|long long) int\)i\]: SUCCESS
+\[main\.pointer_dereference\.1\] line \d+ dereference failure: pointer NULL in a\[(\(signed (long|long long) int\))?i\]: SUCCESS
+\[main\.pointer_dereference\.2\] line \d+ dereference failure: pointer invalid in a\[(\(signed (long|long long) int\))?i\]: SUCCESS
+\[main\.pointer_dereference\.3\] line \d+ dereference failure: deallocated dynamic object in a\[(\(signed (long|long long) int\))?i\]: SUCCESS
+\[main\.pointer_dereference\.4\] line \d+ dereference failure: dead object in a\[(\(signed (long|long long) int\))?i\]: SUCCESS
+\[main\.pointer_dereference\.5\] line \d+ dereference failure: pointer outside object bounds in a\[(\(signed (long|long long) int\))?i\]: SUCCESS
+\[main\.pointer_dereference\.6\] line \d+ dereference failure: invalid integer address in a\[(\(signed (long|long long) int\))?i\]: SUCCESS
 \[main\.assertion.2] line \d+ assertion __CPROVER_forall \{ int j; \!\(0 <= j && j < 1\) || \(j == 0 && \*\(a\+j\) == \*\(a+j\)\) \}: SUCCESS
-\[main\.pointer_dereference\.7] line \d+ dereference failure: pointer NULL in a\[\(signed (long|long long) int\)j\]: SUCCESS
-\[main\.pointer_dereference\.8] line \d+ dereference failure: pointer invalid in a\[\(signed (long|long long) int\)j\]: SUCCESS
-\[main\.pointer_dereference\.9] line \d+ dereference failure: deallocated dynamic object in a\[\(signed (long|long long) int\)j\]: SUCCESS
-\[main\.pointer_dereference\.10] line \d+ dereference failure: dead object in a\[\(signed (long|long long) int\)j\]: SUCCESS
-\[main\.pointer_dereference\.11] line \d+ dereference failure: pointer outside object bounds in a\[\(signed (long|long long) int\)j\]: SUCCESS
-\[main\.pointer_dereference\.12] line \d+ dereference failure: invalid integer address in a\[\(signed (long|long long) int\)j\]: SUCCESS
+\[main\.pointer_dereference\.7] line \d+ dereference failure: pointer NULL in a\[(\(signed (long|long long) int\))?j\]: SUCCESS
+\[main\.pointer_dereference\.8] line \d+ dereference failure: pointer invalid in a\[(\(signed (long|long long) int\))?j\]: SUCCESS
+\[main\.pointer_dereference\.9] line \d+ dereference failure: deallocated dynamic object in a\[(\(signed (long|long long) int\))?j\]: SUCCESS
+\[main\.pointer_dereference\.10] line \d+ dereference failure: dead object in a\[(\(signed (long|long long) int\))?j\]: SUCCESS
+\[main\.pointer_dereference\.11] line \d+ dereference failure: pointer outside object bounds in a\[(\(signed (long|long long) int\))?j\]: SUCCESS
+\[main\.pointer_dereference\.12] line \d+ dereference failure: invalid integer address in a\[(\(signed (long|long long) int\))?j\]: SUCCESS
 ^VERIFICATION SUCCESSFUL$
 --
 --

regression/cbmc-primitives/forall_6231_3/test.desc

@@ -4,12 +4,12 @@ test.c
 ^EXIT=0$
 ^SIGNAL=0$
 \[main\.assertion\.2\] line \d+ assertion __CPROVER_forall \{ int i ; \(0 <= i && i < 10\) ==> \*\(a\+i\) == \*\(a\+i\) \}: SUCCESS
-\[main\.pointer_dereference\.7\] line \d+ dereference failure: pointer NULL in a\[\(signed (long|long long) int\)i\]: SUCCESS
-\[main\.pointer_dereference\.8\] line \d+ dereference failure: pointer invalid in a\[\(signed (long|long long) int\)i\]: SUCCESS
-\[main\.pointer_dereference\.9\] line \d+ dereference failure: deallocated dynamic object in a\[\(signed (long|long long) int\)i\]: SUCCESS
-\[main\.pointer_dereference\.10\] line \d+ dereference failure: dead object in a\[\(signed (long|long long) int\)i\]: SUCCESS
-\[main\.pointer_dereference\.11\] line \d+ dereference failure: pointer outside object bounds in a\[\(signed (long|long long) int\)i\]: SUCCESS
-\[main\.pointer_dereference\.12\] line \d+ dereference failure: invalid integer address in a\[\(signed (long|long long) int\)i\]: SUCCESS
+\[main\.pointer_dereference\.7\] line \d+ dereference failure: pointer NULL in a\[(\(signed (long|long long) int\))?i\]: SUCCESS
+\[main\.pointer_dereference\.8\] line \d+ dereference failure: pointer invalid in a\[(\(signed (long|long long) int\))?i\]: SUCCESS
+\[main\.pointer_dereference\.9\] line \d+ dereference failure: deallocated dynamic object in a\[(\(signed (long|long long) int\))?i\]: SUCCESS
+\[main\.pointer_dereference\.10\] line \d+ dereference failure: dead object in a\[(\(signed (long|long long) int\))?i\]: SUCCESS
+\[main\.pointer_dereference\.11\] line \d+ dereference failure: pointer outside object bounds in a\[(\(signed (long|long long) int\))?i\]: SUCCESS
+\[main\.pointer_dereference\.12\] line \d+ dereference failure: invalid integer address in a\[(\(signed (long|long long) int\))?i\]: SUCCESS
 ^VERIFICATION SUCCESSFUL$
 --
 --

regression/cbmc-primitives/forall_6231_3/test_malloc_less_than_bound.desc

@@ -4,12 +4,12 @@ test_malloc_less_than_bound.c
 ^EXIT=10$
 ^SIGNAL=0$
 \[main\.assertion\.2\] line \d+ assertion __CPROVER_forall \{ int i ; \(0 <= i && i < 10\) ==> \*\(a\+i\) == \*\(a\+i\) \}: SUCCESS
-\[main\.pointer_dereference\.7\] line \d+ dereference failure: pointer NULL in a\[\(signed (long|long long) int\)i\]: SUCCESS
-\[main\.pointer_dereference\.8\] line \d+ dereference failure: pointer invalid in a\[\(signed (long|long long) int\)i\]: SUCCESS
-\[main\.pointer_dereference\.9\] line \d+ dereference failure: deallocated dynamic object in a\[\(signed (long|long long) int\)i\]: SUCCESS
-\[main\.pointer_dereference\.10\] line \d+ dereference failure: dead object in a\[\(signed (long|long long) int\)i\]: SUCCESS
-\[main\.pointer_dereference\.11\] line \d+ dereference failure: pointer outside object bounds in a\[\(signed (long|long long) int\)i\]: FAILURE
-\[main\.pointer_dereference\.12\] line \d+ dereference failure: invalid integer address in a\[\(signed (long|long long) int\)i\]: SUCCESS
+\[main\.pointer_dereference\.7\] line \d+ dereference failure: pointer NULL in a\[(\(signed (long|long long) int\))?i\]: SUCCESS
+\[main\.pointer_dereference\.8\] line \d+ dereference failure: pointer invalid in a\[(\(signed (long|long long) int\))?i\]: SUCCESS
+\[main\.pointer_dereference\.9\] line \d+ dereference failure: deallocated dynamic object in a\[(\(signed (long|long long) int\))?i\]: SUCCESS
+\[main\.pointer_dereference\.10\] line \d+ dereference failure: dead object in a\[(\(signed (long|long long) int\))?i\]: SUCCESS
+\[main\.pointer_dereference\.11\] line \d+ dereference failure: pointer outside object bounds in a\[(\(signed (long|long long) int\))?i\]: FAILURE
+\[main\.pointer_dereference\.12\] line \d+ dereference failure: invalid integer address in a\[(\(signed (long|long long) int\))?i\]: SUCCESS
 ^VERIFICATION FAILED$
 --
 --

regression/cbmc/Pointer2/main.c

@@ -1,10 +1,10 @@
 int main()
 {
   int x;
-  unsigned long long x_i;
+  __CPROVER_size_t x_i;
   _Static_assert(sizeof(&x) == sizeof(x_i), "pointer width");
-  __CPROVER_assert(((unsigned long long)&x & 0x1ULL) == 0, "LSB is zero");
-  x_i = (unsigned long long)&x >> 1;
+  __CPROVER_assert(((__CPROVER_size_t)&x & 0x1ULL) == 0, "LSB is zero");
+  x_i = (__CPROVER_size_t)&x >> 1;
   x_i <<= 1;
   __CPROVER_assert(*(int *)x_i == x, "pointer to x is tracked through shifts");
 }

regression/cbmc/array-cell-sensitivity2/test.desc

@@ -1,7 +1,7 @@
 CORE new-smt-backend
 test.c
 --show-vcc
-main::1::array!0@1#2 = with\(main::1::array!0@1#1, cast\(main::argc!0@1#1 \+ -1, signedbv\[64\]\), 1\)
+main::1::array!0@1#2 = with\(main::1::array!0@1#1, (main::argc!0@1#1 \+ -1|cast\(main::argc!0@1#1 \+ -1, signedbv\[64\]\)), 1\)
 main::1::array!0@1#3 = with\(main::1::array!0@1#2, 1, main::argc!0@1#1\)
 ^EXIT=0$
 ^SIGNAL=0$