diff --git a/.github/workflows/pull-request-checks.yaml b/.github/workflows/pull-request-checks.yaml index 16da79c2ac5..8a3426f987d 100644 --- a/.github/workflows/pull-request-checks.yaml +++ b/.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 diff --git a/regression/cbmc-incr-smt2/arrays_traces/array_write.desc b/regression/cbmc-incr-smt2/arrays_traces/array_write.desc index 19828b6cb11..a39a17baab1 100644 --- a/regression/cbmc-incr-smt2/arrays_traces/array_write.desc +++ b/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$ -- diff --git a/regression/cbmc-incr-smt2/enums/enum_in_array.desc b/regression/cbmc-incr-smt2/enums/enum_in_array.desc index 609e97c87bc..3a57fdcfac9 100644 --- a/regression/cbmc-incr-smt2/enums/enum_in_array.desc +++ b/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$ -- diff --git a/regression/cbmc-incr-smt2/nondeterministic-int-assert/stdout-match.desc b/regression/cbmc-incr-smt2/nondeterministic-int-assert/stdout-match.desc index 30ff29fc589..dda8961be6d 100644 --- a/regression/cbmc-incr-smt2/nondeterministic-int-assert/stdout-match.desc +++ b/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$ diff --git a/regression/cbmc-incr-smt2/pointers-relational-operators/pointers_assume.c b/regression/cbmc-incr-smt2/pointers-relational-operators/pointers_assume.c index 42e2cfbe407..962c4963b8d 100644 --- a/regression/cbmc-incr-smt2/pointers-relational-operators/pointers_assume.c +++ b/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); diff --git a/regression/cbmc-incr-smt2/pointers-relational-operators/pointers_assume.desc b/regression/cbmc-incr-smt2/pointers-relational-operators/pointers_assume.desc index d7c0a231f7c..c66861d774a 100644 --- a/regression/cbmc-incr-smt2/pointers-relational-operators/pointers_assume.desc +++ b/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$ -- diff --git a/regression/cbmc-incr-smt2/pointers/object_size.desc b/regression/cbmc-incr-smt2/pointers/object_size.desc index ee85637ae4d..5f67bfef250 100644 --- a/regression/cbmc-incr-smt2/pointers/object_size.desc +++ b/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$ -- diff --git a/regression/cbmc-incr-smt2/structs/large_array_of_struct_nondet_index.desc b/regression/cbmc-incr-smt2/structs/large_array_of_struct_nondet_index.desc index 7f7d10bd82a..2ad7b44a60d 100644 --- a/regression/cbmc-incr-smt2/structs/large_array_of_struct_nondet_index.desc +++ b/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 diff --git a/regression/cbmc-library/write-01/main.c b/regression/cbmc-library/write-01/main.c index cc7c90ddddb..b55532a540a 100644 --- a/regression/cbmc-library/write-01/main.c +++ b/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); } diff --git a/regression/cbmc-primitives/exists_memory_checks/invalid_index_range.desc b/regression/cbmc-primitives/exists_memory_checks/invalid_index_range.desc index 87795274cf9..09a4b6a7a72 100644 --- a/regression/cbmc-primitives/exists_memory_checks/invalid_index_range.desc +++ b/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 diff --git a/regression/cbmc-primitives/exists_memory_checks/negated_exists.desc b/regression/cbmc-primitives/exists_memory_checks/negated_exists.desc index 8eb7c3431eb..69643c4a532 100644 --- a/regression/cbmc-primitives/exists_memory_checks/negated_exists.desc +++ b/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 diff --git a/regression/cbmc-primitives/exists_memory_checks/smt_missing_range_check.desc b/regression/cbmc-primitives/exists_memory_checks/smt_missing_range_check.desc index 8b0f96e4a8e..e607b134aa9 100644 --- a/regression/cbmc-primitives/exists_memory_checks/smt_missing_range_check.desc +++ b/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 diff --git a/regression/cbmc-primitives/exists_memory_checks/valid_index_range.desc b/regression/cbmc-primitives/exists_memory_checks/valid_index_range.desc index ca59df9ee8f..4701ef529ad 100644 --- a/regression/cbmc-primitives/exists_memory_checks/valid_index_range.desc +++ b/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 diff --git a/regression/cbmc-primitives/forall_6231_1/test.desc b/regression/cbmc-primitives/forall_6231_1/test.desc index 8878c78e929..e7be61857f2 100644 --- a/regression/cbmc-primitives/forall_6231_1/test.desc +++ b/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$ -- -- diff --git a/regression/cbmc-primitives/forall_6231_2/test.desc b/regression/cbmc-primitives/forall_6231_2/test.desc index 4e9a05b367a..0ee5ae2025e 100644 --- a/regression/cbmc-primitives/forall_6231_2/test.desc +++ b/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$ -- -- diff --git a/regression/cbmc-primitives/forall_6231_3/test.desc b/regression/cbmc-primitives/forall_6231_3/test.desc index 1c4424da047..52fd12384f8 100644 --- a/regression/cbmc-primitives/forall_6231_3/test.desc +++ b/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$ -- -- diff --git a/regression/cbmc-primitives/forall_6231_3/test_malloc_less_than_bound.desc b/regression/cbmc-primitives/forall_6231_3/test_malloc_less_than_bound.desc index 8b977e8cbf7..fa1886f8261 100644 --- a/regression/cbmc-primitives/forall_6231_3/test_malloc_less_than_bound.desc +++ b/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$ -- -- diff --git a/regression/cbmc/Pointer2/main.c b/regression/cbmc/Pointer2/main.c index de7e7ba505a..1532625929b 100644 --- a/regression/cbmc/Pointer2/main.c +++ b/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"); } diff --git a/regression/cbmc/array-cell-sensitivity2/test.desc b/regression/cbmc/array-cell-sensitivity2/test.desc index e36c2d65cb0..976c607d8b1 100644 --- a/regression/cbmc/array-cell-sensitivity2/test.desc +++ b/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$ diff --git a/regression/cbmc/array-function-parameters/test.desc b/regression/cbmc/array-function-parameters/test.desc index 769bc7e70a5..515a2470dd8 100644 --- a/regression/cbmc/array-function-parameters/test.desc +++ b/regression/cbmc/array-function-parameters/test.desc @@ -14,6 +14,6 @@ test.c \[test.assertion.9\] line \d+ assertion Test.lists\[0\] != Test.lists\[1\]: SUCCESS \[test.assertion.10\] line \d+ assertion Test.lists\[1\] != Test.lists\[2\]: SUCCESS \[test.assertion.11\] line \d+ assertion Test.lists\[2\] != Test.lists\[3\]: SUCCESS -\[test.array_bounds.1\] line \d+ array 'Test'.lists upper bound in Test.lists\[\(signed long( long)? int\)4\]: FAILURE +\[test.array_bounds.1\] line \d+ array 'Test'.lists upper bound in Test.lists\[(\(signed long( long)? int\))?4\]: FAILURE \[test.assertion.12\] line \d+ assertion !Test.lists\[4\]: FAILURE -- diff --git a/regression/cbmc/array_of_bool_as_bitvec/main.c b/regression/cbmc/array_of_bool_as_bitvec/main.c index 07106dde3d2..e509f41d7c1 100644 --- a/regression/cbmc/array_of_bool_as_bitvec/main.c +++ b/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]); diff --git a/regression/cbmc/array_of_bool_as_bitvec/test-smt2-outfile.desc b/regression/cbmc/array_of_bool_as_bitvec/test-smt2-outfile.desc index a7ede3fc945..16474b90ac5 100644 --- a/regression/cbmc/array_of_bool_as_bitvec/test-smt2-outfile.desc +++ b/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. diff --git a/regression/cbmc/assigning_nullpointers_should_not_crash_symex/main.c b/regression/cbmc/assigning_nullpointers_should_not_crash_symex/main.c index c299daccfff..fb04178ca9f 100644 --- a/regression/cbmc/assigning_nullpointers_should_not_crash_symex/main.c +++ b/regression/cbmc/assigning_nullpointers_should_not_crash_symex/main.c @@ -6,9 +6,19 @@ struct linked_list struct linked_list *next; }; +#ifdef _WIN32 +# ifdef _M_X64 +# define POINTER_BYTES 8ul +# else +# define POINTER_BYTES 4ul +# endif +#else +# define POINTER_BYTES __SIZEOF_POINTER__ +#endif + int main(void) { - size_t list_sz = 8ul; + size_t list_sz = POINTER_BYTES; assert(list_sz == sizeof(struct linked_list)); struct linked_list *list = malloc(list_sz); // this line makes symex crash for some reason diff --git a/regression/cbmc/bounds_check2/test.desc b/regression/cbmc/bounds_check2/test.desc index 67ec0a948f9..32b1f9a2f71 100644 --- a/regression/cbmc/bounds_check2/test.desc +++ b/regression/cbmc/bounds_check2/test.desc @@ -2,7 +2,7 @@ CORE new-smt-backend main.c --bounds-check --retain-trivial-checks ^Generated \d+ VCC\(s\), 0 remaining after simplification$ -^\[main.array_bounds.1\] line 4 array 'A' lower bound in A\[\(signed (long (long )?)?int\)1\]: SUCCESS$ +^\[main.array_bounds.1\] line 4 array 'A' (lower|upper) bound in A\[(\(signed (long (long )?)?int\))?1\]: SUCCESS$ ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/cbmc/byte_update11/main.c b/regression/cbmc/byte_update11/main.c index 18d0ebc517d..02bcf96660a 100644 --- a/regression/cbmc/byte_update11/main.c +++ b/regression/cbmc/byte_update11/main.c @@ -5,7 +5,8 @@ struct S int main() { - unsigned x; + int x; + __CPROVER_assume(x >= 0); __CPROVER_assume(x % sizeof(int) == 0); struct S A[x]; ((char *)A)[x] = 42; diff --git a/regression/cbmc/double_deref/double_deref_with_pointer_arithmetic.desc b/regression/cbmc/double_deref/double_deref_with_pointer_arithmetic.desc index a0033264617..c0d895cda47 100644 --- a/regression/cbmc/double_deref/double_deref_with_pointer_arithmetic.desc +++ b/regression/cbmc/double_deref/double_deref_with_pointer_arithmetic.desc @@ -1,7 +1,7 @@ CORE new-smt-backend double_deref_with_pointer_arithmetic.c --show-vcc -^\{-[0-9]+\} derefd_pointer::derefd_pointer!0#1 = \{ symex_dynamic::dynamic_object#3\[\[0\]\], symex_dynamic::dynamic_object#3\[\[1\]\] \}\[cast\(mod\(main::argc!0@1#1, 2\), signedbv\[64\]\)\] +^\{-[0-9]+\} derefd_pointer::derefd_pointer!0#1 = \{ symex_dynamic::dynamic_object#3\[\[0\]\], symex_dynamic::dynamic_object#3\[\[1\]\] \}\[(mod\(main::argc!0@1#1, 2\)|cast\(mod\(main::argc!0@1#1, 2\), signedbv\[64\]\))\] ^\{1\} \(derefd_pointer::derefd_pointer!0#1 = address_of\(symex_dynamic::dynamic_object\$[01]\) \? main::argc!0@1#1 = 2 : \(derefd_pointer::derefd_pointer!0#1 = address_of\(symex_dynamic::dynamic_object\$[01]\) \? main::argc!0@1#1 = 1 : symex::invalid_object!0#0 = main::argc!0@1#1\)\) ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/cbmc/gcc_builtin_sub_overflow/main.c b/regression/cbmc/gcc_builtin_sub_overflow/main.c index 28e8fce2df0..8370657160b 100644 --- a/regression/cbmc/gcc_builtin_sub_overflow/main.c +++ b/regression/cbmc/gcc_builtin_sub_overflow/main.c @@ -39,7 +39,7 @@ void check_long(void) void check_long_long(void) { - long result; + long long result; assert(!__builtin_ssubll_overflow(1ll, 1ll, &result)); assert(result == 0ll); assert(__builtin_ssubll_overflow(LLONG_MIN, 1ll, &result)); diff --git a/regression/cbmc/graphml_witness2/test.desc b/regression/cbmc/graphml_witness2/test.desc index 2cae2c296bb..b31243fbb28 100644 --- a/regression/cbmc/graphml_witness2/test.desc +++ b/regression/cbmc/graphml_witness2/test.desc @@ -4,7 +4,7 @@ main.c ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ -foo = \(\(unsigned long( long)? int \*\)0\); +foo = \(\(unsigned( long( long)?)? int \*\)0\); one -- ^warning: ignoring diff --git a/regression/cbmc/havoc_slice/test_struct_raw_bytes.c b/regression/cbmc/havoc_slice/test_struct_raw_bytes.c index 1920cc771ed..20339a02a96 100644 --- a/regression/cbmc/havoc_slice/test_struct_raw_bytes.c +++ b/regression/cbmc/havoc_slice/test_struct_raw_bytes.c @@ -36,6 +36,6 @@ void main(void) __CPROVER_assert(c[16] == old_c[16], "expecting FAILURE"); __CPROVER_assert(c[17] == old_c[17], "expecting FAILURE"); __CPROVER_assert(c[18] == old_c[18], "expecting SUCCESS"); - __CPROVER_assert(c[19] == old_c[20], "expecting SUCCESS"); + __CPROVER_assert(c[19] == old_c[19], "expecting SUCCESS"); return; } diff --git a/regression/cbmc/memory_allocation2/test.desc b/regression/cbmc/memory_allocation2/test.desc index 7cb66ccaaef..e0d2061483c 100644 --- a/regression/cbmc/memory_allocation2/test.desc +++ b/regression/cbmc/memory_allocation2/test.desc @@ -4,7 +4,7 @@ main.c ^EXIT=10$ ^SIGNAL=0$ ^\[main\.array_bounds\.[1-2]\] .*: SUCCESS$ -^\[main\.array_bounds\.3\] line 38 array.buffer (dynamic object )?upper bound in buffers\[\(signed long (long )?int\)0\]->buffer\[\(signed long (long )?int\)100\]: FAILURE$ +^\[main\.array_bounds\.3\] line 38 array.buffer (dynamic object )?upper bound in buffers\[(\(signed long (long )?int\))?0\]->buffer\[(\(signed long (long )?int\))?100\]: FAILURE$ ^\*\* 1 of 3 failed ^VERIFICATION FAILED$ -- diff --git a/regression/cbmc/pointer-overflow2/test.desc b/regression/cbmc/pointer-overflow2/test.desc index 2f2365bd2fb..cc01b9c5024 100644 --- a/regression/cbmc/pointer-overflow2/test.desc +++ b/regression/cbmc/pointer-overflow2/test.desc @@ -3,9 +3,9 @@ main.c --pointer-overflow-check ^EXIT=0$ ^SIGNAL=0$ -\[main.pointer_arithmetic.1\] line \d+ pointer arithmetic: invalid integer address in p - \(signed long (long )?int\)1: SUCCESS -\[main.pointer_arithmetic.2\] line \d+ pointer arithmetic: invalid integer address in p \+ \(signed long (long )?int\)1: SUCCESS -\[main.pointer_arithmetic.3\] line \d+ pointer arithmetic: invalid integer address in p \+ \(signed long (long )?int\)-1: SUCCESS -\[main.pointer_arithmetic.4\] line \d+ pointer arithmetic: invalid integer address in p - \(signed long (long )?int\)-1: SUCCESS +\[main.pointer_arithmetic.1\] line \d+ pointer arithmetic: invalid integer address in p - (\(signed long (long )?int\))?1: SUCCESS +\[main.pointer_arithmetic.2\] line \d+ pointer arithmetic: invalid integer address in p \+ (\(signed long (long )?int\))?1: SUCCESS +\[main.pointer_arithmetic.3\] line \d+ pointer arithmetic: invalid integer address in p \+ (\(signed long (long )?int\))?-1: SUCCESS +\[main.pointer_arithmetic.4\] line \d+ pointer arithmetic: invalid integer address in p - (\(signed long (long )?int\))?-1: SUCCESS -- ^warning: ignoring diff --git a/regression/cbmc/pointer-overflow3/no-simplify.desc b/regression/cbmc/pointer-overflow3/no-simplify.desc index 220660e5ddb..fb659529422 100644 --- a/regression/cbmc/pointer-overflow3/no-simplify.desc +++ b/regression/cbmc/pointer-overflow3/no-simplify.desc @@ -1,10 +1,10 @@ CORE main.c --pointer-overflow-check --no-simplify -^\[main.pointer_arithmetic.\d+\] line 6 pointer arithmetic: pointer outside object bounds in p \+ \(signed (long (long )?)?int\)10: FAILURE -^\[main.pointer_arithmetic.\d+\] line 7 pointer arithmetic: pointer outside object bounds in p - \(signed (long (long )?)?int\)10: FAILURE -^\[main.pointer_arithmetic.\d+\] line 10 pointer arithmetic: pointer outside object bounds in arr \+ \(signed (long (long )?)?int\)10: FAILURE -^\[main.pointer_arithmetic.\d+\] line 11 pointer arithmetic: pointer outside object bounds in arr - \(signed (long (long )?)?int\)10: FAILURE +^\[main.pointer_arithmetic.\d+\] line 6 pointer arithmetic: pointer outside object bounds in p \+ (\(signed (long (long )?)?int\))?10: FAILURE +^\[main.pointer_arithmetic.\d+\] line 7 pointer arithmetic: pointer outside object bounds in p - (\(signed (long (long )?)?int\))?10: FAILURE +^\[main.pointer_arithmetic.\d+\] line 10 pointer arithmetic: pointer outside object bounds in arr \+ (\(signed (long (long )?)?int\))?10: FAILURE +^\[main.pointer_arithmetic.\d+\] line 11 pointer arithmetic: pointer outside object bounds in arr - (\(signed (long (long )?)?int\))?10: FAILURE ^\*\* 4 of \d+ failed ^VERIFICATION FAILED$ ^EXIT=10$ diff --git a/regression/cbmc/pointer-overflow3/test.desc b/regression/cbmc/pointer-overflow3/test.desc index 71c50f53cf1..e781ff58a46 100644 --- a/regression/cbmc/pointer-overflow3/test.desc +++ b/regression/cbmc/pointer-overflow3/test.desc @@ -1,10 +1,10 @@ CORE new-smt-backend main.c --pointer-overflow-check -^\[main.pointer_arithmetic.\d+\] line 6 pointer arithmetic: pointer outside object bounds in p \+ \(signed (long (long )?)?int\)10: FAILURE -^\[main.pointer_arithmetic.\d+\] line 7 pointer arithmetic: pointer outside object bounds in p - \(signed (long (long )?)?int\)10: FAILURE -^\[main.pointer_arithmetic.\d+\] line 10 pointer arithmetic: pointer outside object bounds in arr \+ \(signed (long (long )?)?int\)10: FAILURE -^\[main.pointer_arithmetic.\d+\] line 11 pointer arithmetic: pointer outside object bounds in arr - \(signed (long (long )?)?int\)10: FAILURE +^\[main.pointer_arithmetic.\d+\] line 6 pointer arithmetic: pointer outside object bounds in p \+ (\(signed (long (long )?)?int\))?10: FAILURE +^\[main.pointer_arithmetic.\d+\] line 7 pointer arithmetic: pointer outside object bounds in p - (\(signed (long (long )?)?int\))?10: FAILURE +^\[main.pointer_arithmetic.\d+\] line 10 pointer arithmetic: pointer outside object bounds in arr \+ (\(signed (long (long )?)?int\))?10: FAILURE +^\[main.pointer_arithmetic.\d+\] line 11 pointer arithmetic: pointer outside object bounds in arr - (\(signed (long (long )?)?int\))?10: FAILURE ^\*\* 4 of \d+ failed ^VERIFICATION FAILED$ ^EXIT=10$ diff --git a/regression/cbmc/pragma_cprover1/test.desc b/regression/cbmc/pragma_cprover1/test.desc index 64834a9dde9..a7d256af3c6 100644 --- a/regression/cbmc/pragma_cprover1/test.desc +++ b/regression/cbmc/pragma_cprover1/test.desc @@ -1,7 +1,7 @@ CORE new-smt-backend main.c --signed-overflow-check --bounds-check -line 14 array 'y' upper bound in y\[\(signed long( long)? int\)1\]: FAILURE$ +line 14 array 'y' upper bound in y\[(\(signed long( long)? int\))?1\]: FAILURE$ ^\*\* 1 of 1 failed ^VERIFICATION FAILED$ ^EXIT=10$ diff --git a/regression/cbmc/pragma_cprover_enable_all/test.desc b/regression/cbmc/pragma_cprover_enable_all/test.desc index 1dcd0b7e9ca..be5658ae717 100644 --- a/regression/cbmc/pragma_cprover_enable_all/test.desc +++ b/regression/cbmc/pragma_cprover_enable_all/test.desc @@ -3,7 +3,7 @@ main.c --object-bits 8 --bounds-check --pointer-check --pointer-primitive-check --div-by-zero-check --enum-range-check --unsigned-overflow-check --signed-overflow-check --pointer-overflow-check --float-overflow-check --conversion-check --undefined-shift-check --nan-check --pointer-primitive-check ^\[main\.pointer_primitives\.\d+\] line 77 pointer invalid in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$ ^\[main\.pointer_primitives\.\d+\] line 77 pointer outside object bounds in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$ -^\[main\.pointer_arithmetic\.\d+\] line 78 pointer arithmetic: pointer outside object bounds in p \+ 2000000000000(l|ll): FAILURE +^\[main\.pointer_arithmetic\.\d+\] line 78 pointer arithmetic: pointer outside object bounds in p \+ (\(signed int\))?2000000000000(l|ll): FAILURE ^\[main\.NaN\.\d+\] line 84 NaN on / in x / den: FAILURE ^\[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 @@ -16,7 +16,7 @@ main.c -- ^\[main\.pointer_primitives\.\d+\] line 40 pointer invalid in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$ ^\[main\.pointer_primitives\.\d+\] line 40 pointer outside object bounds in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$ -^\[main\.pointer_arithmetic\.\d+\] line 41 pointer arithmetic: pointer outside object bounds in p \+ 2000000000000(l|ll): FAILURE +^\[main\.pointer_arithmetic\.\d+\] line 41 pointer arithmetic: pointer outside object bounds in p \+ .*2000000000000(l|ll): FAILURE ^\[main\.NaN\.\d+\] line 47 NaN on / in x / den: FAILURE ^\[main\.division-by-zero\.\d+\] line 47 division by zero in x / den: FAILURE ^\[main\.overflow\.\d+\] line 47 arithmetic overflow on floating-point division in x / den: FAILURE diff --git a/regression/cbmc/ptr_arithmetic_on_null/main.c b/regression/cbmc/ptr_arithmetic_on_null/main.c index bbb7082c70c..339617ec6c7 100644 --- a/regression/cbmc/ptr_arithmetic_on_null/main.c +++ b/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)); diff --git a/regression/cbmc/ptr_arithmetic_on_null/test.desc b/regression/cbmc/ptr_arithmetic_on_null/test.desc index 1e01d37c22b..b7c0190dbc5 100644 --- a/regression/cbmc/ptr_arithmetic_on_null/test.desc +++ b/regression/cbmc/ptr_arithmetic_on_null/test.desc @@ -1,13 +1,13 @@ CORE gcc-only 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.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.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$ -^\[main.assertion.7\] line .* assertion \(ptr - \(.*\)1\) \+ \(.*\)1 == \(\(.* \*\)NULL\): FAILURE$ +^\[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$ +^\[main.assertion.7\] line .* assertion \(ptr - (\(.*\))?1\) \+ (\(.*\))?1 == \(\(.* \*\)NULL\): FAILURE$ ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/cbmc/return9/test.desc b/regression/cbmc/return9/test.desc index 5ca4807ec69..a252bdd17d7 100644 --- a/regression/cbmc/return9/test.desc +++ b/regression/cbmc/return9/test.desc @@ -4,5 +4,5 @@ tcas_v23_523.c ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ -^\[ALIM.array_bounds.2\] line 68 array 'Positive_RA_Alt_Thresh' upper bound in Positive_RA_Alt_Thresh\[\(signed (long (long )?)?int\)Alt_Layer_Value\]: FAILURE$ +^\[ALIM.array_bounds.2\] line 68 array 'Positive_RA_Alt_Thresh' upper bound in Positive_RA_Alt_Thresh\[(\(signed (long (long )?)?int\))?Alt_Layer_Value\]: FAILURE$ -- diff --git a/regression/cbmc/simplify_singleton_interval_7690/singleton_interval_in_assume_7690.c b/regression/cbmc/simplify_singleton_interval_7690/singleton_interval_in_assume_7690.c index 37a264e7d63..f382fe03dfb 100644 --- a/regression/cbmc/simplify_singleton_interval_7690/singleton_interval_in_assume_7690.c +++ b/regression/cbmc/simplify_singleton_interval_7690/singleton_interval_in_assume_7690.c @@ -6,10 +6,16 @@ #include extern size_t __CPROVER_max_malloc_size; -int __builtin_clzll(unsigned long long); +#if defined(_WIN32) && defined(_M_X64) +int __builtin_clzll(unsigned long long); #define __nof_symex_objects \ ((size_t)(1ULL << __builtin_clzll(__CPROVER_max_malloc_size))) +#else +int __builtin_clzl(unsigned long); +#define __nof_symex_objects \ + ((size_t)(1UL << __builtin_clzl(__CPROVER_max_malloc_size))) +#endif typedef struct { size_t k; diff --git a/regression/cbmc/simplify_singleton_interval_7690/test_smt2.desc b/regression/cbmc/simplify_singleton_interval_7690/test_smt2.desc index 3f31b18e144..2563cfc11bc 100644 --- a/regression/cbmc/simplify_singleton_interval_7690/test_smt2.desc +++ b/regression/cbmc/simplify_singleton_interval_7690/test_smt2.desc @@ -1,7 +1,7 @@ CORE smt-backend new-smt-backend singleton_interval_in_assume_7690.c --pointer-check -^\[stk_push\.pointer_dereference\.17] line \d+ dereference failure: pointer outside object bounds in stk-\>elems\[\(signed (long|long long) int\)stk-\>top\]: SUCCESS$ +^\[stk_push\.pointer_dereference\.17] line \d+ dereference failure: pointer outside object bounds in stk-\>elems\[\(signed( long( long)?)? int\)stk-\>top\]: SUCCESS$ ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/contracts-dfcc/assigns-enforce-malloc-zero/test.desc b/regression/contracts-dfcc/assigns-enforce-malloc-zero/test.desc index db64e5e4568..d15c7b71e28 100644 --- a/regression/contracts-dfcc/assigns-enforce-malloc-zero/test.desc +++ b/regression/contracts-dfcc/assigns-enforce-malloc-zero/test.desc @@ -1,7 +1,7 @@ CORE dfcc-only main.c --malloc-may-fail --malloc-fail-null --dfcc main --enforce-contract foo -^\[foo.assigns.\d+\] line \d+ Check that a\[\(signed long (long )?int\)i\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line \d+ Check that a\[(\(signed (long (long )?)?int\))?i\] is assignable: SUCCESS$ ^\[foo.assigns.\d+\] line \d+ Check that \*out is assignable: SUCCESS$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/contracts-dfcc/assigns-frees-clauses-check-side-effects/test.desc b/regression/contracts-dfcc/assigns-frees-clauses-check-side-effects/test.desc index dd2519f56dd..7470ab2abc3 100644 --- a/regression/contracts-dfcc/assigns-frees-clauses-check-side-effects/test.desc +++ b/regression/contracts-dfcc/assigns-frees-clauses-check-side-effects/test.desc @@ -1,8 +1,8 @@ CORE dfcc-only main.c --dfcc main --enforce-contract foo --malloc-may-fail --malloc-fail-null -^\[foo_assigns.assigns.\d+\] line \d+ Check that ptr\[\(.* int\)0\] is assignable: FAILURE$ -^\[foo_frees.assigns.\d+\] line \d+ Check that ptr\[\(.* int\)0\] is assignable: FAILURE$ +^\[foo_assigns.assigns.\d+\] line \d+ Check that ptr\[(\(.* int\))?0\] is assignable: FAILURE$ +^\[foo_frees.assigns.\d+\] line \d+ Check that ptr\[(\(.* int\))?0\] is assignable: FAILURE$ ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/contracts-dfcc/assigns-slice-targets/test-enforce.desc b/regression/contracts-dfcc/assigns-slice-targets/test-enforce.desc index e1df873e83e..34e4229fad0 100644 --- a/regression/contracts-dfcc/assigns-slice-targets/test-enforce.desc +++ b/regression/contracts-dfcc/assigns-slice-targets/test-enforce.desc @@ -1,33 +1,33 @@ CORE main-enforce.c --dfcc main --enforce-contract foo -^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)0\] is assignable: SUCCESS$ -^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)1\] is assignable: SUCCESS$ -^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)2\] is assignable: SUCCESS$ -^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)3\] is assignable: SUCCESS$ -^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)4\] is assignable: SUCCESS$ -^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)5\] is assignable: FAILURE$ -^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)6\] is assignable: FAILURE$ -^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)7\] is assignable: FAILURE$ -^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)8\] is assignable: FAILURE$ -^\[foo.assigns.\d+\].* Check that s->arr1\[\(.*\)9\] is assignable: FAILURE$ -^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)0\] is assignable: FAILURE$ -^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)1\] is assignable: FAILURE$ -^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)2\] is assignable: FAILURE$ -^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)3\] is assignable: FAILURE$ -^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)4\] is assignable: FAILURE$ -^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)5\] is assignable: SUCCESS$ -^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)6\] is assignable: SUCCESS$ -^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)7\] is assignable: SUCCESS$ -^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)8\] is assignable: SUCCESS$ -^\[foo.assigns.\d+\].* Check that s->arr2\[\(.*\)9\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\].* Check that s->arr1\[(\(.*\))?0\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\].* Check that s->arr1\[(\(.*\))?1\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\].* Check that s->arr1\[(\(.*\))?2\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\].* Check that s->arr1\[(\(.*\))?3\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\].* Check that s->arr1\[(\(.*\))?4\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\].* Check that s->arr1\[(\(.*\))?5\] is assignable: FAILURE$ +^\[foo.assigns.\d+\].* Check that s->arr1\[(\(.*\))?6\] is assignable: FAILURE$ +^\[foo.assigns.\d+\].* Check that s->arr1\[(\(.*\))?7\] is assignable: FAILURE$ +^\[foo.assigns.\d+\].* Check that s->arr1\[(\(.*\))?8\] is assignable: FAILURE$ +^\[foo.assigns.\d+\].* Check that s->arr1\[(\(.*\))?9\] is assignable: FAILURE$ +^\[foo.assigns.\d+\].* Check that s->arr2\[(\(.*\))?0\] is assignable: FAILURE$ +^\[foo.assigns.\d+\].* Check that s->arr2\[(\(.*\))?1\] is assignable: FAILURE$ +^\[foo.assigns.\d+\].* Check that s->arr2\[(\(.*\))?2\] is assignable: FAILURE$ +^\[foo.assigns.\d+\].* Check that s->arr2\[(\(.*\))?3\] is assignable: FAILURE$ +^\[foo.assigns.\d+\].* Check that s->arr2\[(\(.*\))?4\] is assignable: FAILURE$ +^\[foo.assigns.\d+\].* Check that s->arr2\[(\(.*\))?5\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\].* Check that s->arr2\[(\(.*\))?6\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\].* Check that s->arr2\[(\(.*\))?7\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\].* Check that s->arr2\[(\(.*\))?8\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\].* Check that s->arr2\[(\(.*\))?9\] is assignable: SUCCESS$ ^\[foo.assigns.\d+\].* Check that ss->a is assignable: SUCCESS$ -^\[foo.assigns.\d+\].* Check that ss->arr1\[\(.*\)0\] is assignable: SUCCESS$ -^\[foo.assigns.\d+\].* Check that ss->arr1\[\(.*\)7\] is assignable: SUCCESS$ -^\[foo.assigns.\d+\].* Check that ss->arr1\[\(.*\)9\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\].* Check that ss->arr1\[(\(.*\))?0\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\].* Check that ss->arr1\[(\(.*\))?7\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\].* Check that ss->arr1\[(\(.*\))?9\] is assignable: SUCCESS$ ^\[foo.assigns.\d+\].* Check that ss->b is assignable: SUCCESS$ -^\[foo.assigns.\d+\].* Check that ss->arr2\[\(.*\)6\] is assignable: SUCCESS$ -^\[foo.assigns.\d+\].* Check that ss->arr2\[\(.*\)8\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\].* Check that ss->arr2\[(\(.*\))?6\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\].* Check that ss->arr2\[(\(.*\))?8\] is assignable: SUCCESS$ ^\[foo.assigns.\d+\].* Check that ss->c is assignable: SUCCESS$ ^VERIFICATION FAILED$ ^EXIT=10$ diff --git a/regression/contracts-dfcc/assigns-slice-targets/test-replace.desc b/regression/contracts-dfcc/assigns-slice-targets/test-replace.desc index b1eeafd252c..a26bb4b83fb 100644 --- a/regression/contracts-dfcc/assigns-slice-targets/test-replace.desc +++ b/regression/contracts-dfcc/assigns-slice-targets/test-replace.desc @@ -2,50 +2,50 @@ CORE main-replace.c --dfcc main --replace-call-with-contract foo ^\[main.assertion.\d+\].*assertion s.a == 0: SUCCESS$ -^\[main.assertion.\d+\].*assertion \(.*\)s.arr1\[\(.*\)0\] == 0: FAILURE$ -^\[main.assertion.\d+\].*assertion \(.*\)s.arr1\[\(.*\)1\] == 0: FAILURE$ -^\[main.assertion.\d+\].*assertion \(.*\)s.arr1\[\(.*\)2\] == 0: FAILURE$ -^\[main.assertion.\d+\].*assertion \(.*\)s.arr1\[\(.*\)3\] == 0: FAILURE$ -^\[main.assertion.\d+\].*assertion \(.*\)s.arr1\[\(.*\)4\] == 0: FAILURE$ -^\[main.assertion.\d+\].*assertion \(.*\)s.arr1\[\(.*\)5\] == 0: SUCCESS$ -^\[main.assertion.\d+\].*assertion \(.*\)s.arr1\[\(.*\)6\] == 0: SUCCESS$ -^\[main.assertion.\d+\].*assertion \(.*\)s.arr1\[\(.*\)7\] == 0: SUCCESS$ -^\[main.assertion.\d+\].*assertion \(.*\)s.arr1\[\(.*\)8\] == 0: SUCCESS$ -^\[main.assertion.\d+\].*assertion \(.*\)s.arr1\[\(.*\)9\] == 0: SUCCESS$ +^\[main.assertion.\d+\].*assertion \(.*\)s.arr1\[(\(.*\))?0\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)s.arr1\[(\(.*\))?1\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)s.arr1\[(\(.*\))?2\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)s.arr1\[(\(.*\))?3\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)s.arr1\[(\(.*\))?4\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)s.arr1\[(\(.*\))?5\] == 0: SUCCESS$ +^\[main.assertion.\d+\].*assertion \(.*\)s.arr1\[(\(.*\))?6\] == 0: SUCCESS$ +^\[main.assertion.\d+\].*assertion \(.*\)s.arr1\[(\(.*\))?7\] == 0: SUCCESS$ +^\[main.assertion.\d+\].*assertion \(.*\)s.arr1\[(\(.*\))?8\] == 0: SUCCESS$ +^\[main.assertion.\d+\].*assertion \(.*\)s.arr1\[(\(.*\))?9\] == 0: SUCCESS$ ^\[main.assertion.\d+\].*assertion s.b == 0: FAILURE$ -^\[main.assertion.\d+\].*assertion \(.*\)s.arr2\[\(.*\)0\] == 0: SUCCESS$ -^\[main.assertion.\d+\].*assertion \(.*\)s.arr2\[\(.*\)1\] == 0: SUCCESS$ -^\[main.assertion.\d+\].*assertion \(.*\)s.arr2\[\(.*\)2\] == 0: SUCCESS$ -^\[main.assertion.\d+\].*assertion \(.*\)s.arr2\[\(.*\)3\] == 0: SUCCESS$ -^\[main.assertion.\d+\].*assertion \(.*\)s.arr2\[\(.*\)4\] == 0: SUCCESS$ -^\[main.assertion.\d+\].*assertion \(.*\)s.arr2\[\(.*\)5\] == 0: FAILURE$ -^\[main.assertion.\d+\].*assertion \(.*\)s.arr2\[\(.*\)6\] == 0: FAILURE$ -^\[main.assertion.\d+\].*assertion \(.*\)s.arr2\[\(.*\)7\] == 0: FAILURE$ -^\[main.assertion.\d+\].*assertion \(.*\)s.arr2\[\(.*\)8\] == 0: FAILURE$ -^\[main.assertion.\d+\].*assertion \(.*\)s.arr2\[\(.*\)9\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)s.arr2\[(\(.*\))?0\] == 0: SUCCESS$ +^\[main.assertion.\d+\].*assertion \(.*\)s.arr2\[(\(.*\))?1\] == 0: SUCCESS$ +^\[main.assertion.\d+\].*assertion \(.*\)s.arr2\[(\(.*\))?2\] == 0: SUCCESS$ +^\[main.assertion.\d+\].*assertion \(.*\)s.arr2\[(\(.*\))?3\] == 0: SUCCESS$ +^\[main.assertion.\d+\].*assertion \(.*\)s.arr2\[(\(.*\))?4\] == 0: SUCCESS$ +^\[main.assertion.\d+\].*assertion \(.*\)s.arr2\[(\(.*\))?5\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)s.arr2\[(\(.*\))?6\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)s.arr2\[(\(.*\))?7\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)s.arr2\[(\(.*\))?8\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)s.arr2\[(\(.*\))?9\] == 0: FAILURE$ ^\[main.assertion.\d+\].*assertion s.c == 0: FAILURE$ ^\[main.assertion.\d+\].*assertion ss.a == 0: FAILURE$ -^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[\(.*\)0\] == 0: FAILURE$ -^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[\(.*\)1\] == 0: FAILURE$ -^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[\(.*\)2\] == 0: FAILURE$ -^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[\(.*\)3\] == 0: FAILURE$ -^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[\(.*\)4\] == 0: FAILURE$ -^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[\(.*\)5\] == 0: FAILURE$ -^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[\(.*\)6\] == 0: FAILURE$ -^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[\(.*\)7\] == 0: FAILURE$ -^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[\(.*\)8\] == 0: FAILURE$ -^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[\(.*\)9\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[(\(.*\))?0\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[(\(.*\))?1\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[(\(.*\))?2\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[(\(.*\))?3\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[(\(.*\))?4\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[(\(.*\))?5\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[(\(.*\))?6\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[(\(.*\))?7\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[(\(.*\))?8\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)ss.arr1\[(\(.*\))?9\] == 0: FAILURE$ ^\[main.assertion.\d+\].*assertion ss.b == 0: FAILURE$ -^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[\(.*\)0\] == 0: FAILURE$ -^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[\(.*\)1\] == 0: FAILURE$ -^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[\(.*\)2\] == 0: FAILURE$ -^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[\(.*\)3\] == 0: FAILURE$ -^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[\(.*\)4\] == 0: FAILURE$ -^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[\(.*\)5\] == 0: FAILURE$ -^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[\(.*\)6\] == 0: FAILURE$ -^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[\(.*\)7\] == 0: FAILURE$ -^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[\(.*\)8\] == 0: FAILURE$ -^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[\(.*\)9\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[(\(.*\))?0\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[(\(.*\))?1\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[(\(.*\))?2\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[(\(.*\))?3\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[(\(.*\))?4\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[(\(.*\))?5\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[(\(.*\))?6\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[(\(.*\))?7\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[(\(.*\))?8\] == 0: FAILURE$ +^\[main.assertion.\d+\].*assertion \(.*\)ss.arr2\[(\(.*\))?9\] == 0: FAILURE$ ^\[main.assertion.\d+\].*assertion ss.c == 0: FAILURE$ ^VERIFICATION FAILED$ ^EXIT=10$ diff --git a/regression/contracts-dfcc/assigns_enforce_conditional_pointer_object/test.desc b/regression/contracts-dfcc/assigns_enforce_conditional_pointer_object/test.desc index d45cb3bddbf..2faf0c687b4 100644 --- a/regression/contracts-dfcc/assigns_enforce_conditional_pointer_object/test.desc +++ b/regression/contracts-dfcc/assigns_enforce_conditional_pointer_object/test.desc @@ -2,12 +2,12 @@ CORE dfcc-only main.c --dfcc main --enforce-contract foo main.c function foo -^\[foo.assigns.\d+\] line 13 Check that x\[\(signed (long )?long int\)0\] is assignable: SUCCESS$ -^\[foo.assigns.\d+\] line 14 Check that y\[\(signed (long )?long int\)0\] is assignable: FAILURE$ -^\[foo.assigns.\d+\] line 18 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$ -^\[foo.assigns.\d+\] line 19 Check that y\[\(signed (long )?long int\)0\] is assignable: SUCCESS$ -^\[foo.assigns.\d+\] line 22 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$ -^\[foo.assigns.\d+\] line 23 Check that y\[\(signed (long )?long int\)0\] is assignable: FAILURE$ +^\[foo.assigns.\d+\] line 13 Check that x\[(\(signed (long )?long int\))?0\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line 14 Check that y\[(\(signed (long )?long int\))?0\] is assignable: FAILURE$ +^\[foo.assigns.\d+\] line 18 Check that x\[(\(signed (long )?long int\))?0\] is assignable: FAILURE$ +^\[foo.assigns.\d+\] line 19 Check that y\[(\(signed (long )?long int\))?0\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line 22 Check that x\[(\(signed (long )?long int\))?0\] is assignable: FAILURE$ +^\[foo.assigns.\d+\] line 23 Check that y\[(\(signed (long )?long int\))?0\] is assignable: FAILURE$ ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/contracts-dfcc/assigns_enforce_conditional_pointer_object_list/test.desc b/regression/contracts-dfcc/assigns_enforce_conditional_pointer_object_list/test.desc index 73812da891d..d831cc5c367 100644 --- a/regression/contracts-dfcc/assigns_enforce_conditional_pointer_object_list/test.desc +++ b/regression/contracts-dfcc/assigns_enforce_conditional_pointer_object_list/test.desc @@ -2,12 +2,12 @@ CORE dfcc-only main.c --dfcc main --enforce-contract foo main.c function foo -^\[foo.assigns.\d+\] line 12 Check that x\[\(signed (long )?long int\)0\] is assignable: SUCCESS$ -^\[foo.assigns.\d+\] line 13 Check that y\[\(signed (long )?long int\)0\] is assignable: SUCCESS$ -^\[foo.assigns.\d+\] line 17 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$ -^\[foo.assigns.\d+\] line 18 Check that y\[\(signed (long )?long int\)0\] is assignable: FAILURE$ -^\[foo.assigns.\d+\] line 21 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$ -^\[foo.assigns.\d+\] line 22 Check that y\[\(signed (long )?long int\)0\] is assignable: FAILURE$ +^\[foo.assigns.\d+\] line 12 Check that x\[(\(signed (long )?long int\))?0\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line 13 Check that y\[(\(signed (long )?long int\))?0\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line 17 Check that x\[(\(signed (long )?long int\))?0\] is assignable: FAILURE$ +^\[foo.assigns.\d+\] line 18 Check that y\[(\(signed (long )?long int\))?0\] is assignable: FAILURE$ +^\[foo.assigns.\d+\] line 21 Check that x\[(\(signed (long )?long int\))?0\] is assignable: FAILURE$ +^\[foo.assigns.\d+\] line 22 Check that y\[(\(signed (long )?long int\))?0\] is assignable: FAILURE$ ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/contracts-dfcc/assigns_enforce_offsets_2/test.desc b/regression/contracts-dfcc/assigns_enforce_offsets_2/test.desc index ce6b1e21ea3..5eece5b16f2 100644 --- a/regression/contracts-dfcc/assigns_enforce_offsets_2/test.desc +++ b/regression/contracts-dfcc/assigns_enforce_offsets_2/test.desc @@ -1,8 +1,8 @@ CORE dfcc-only main.c --dfcc main --enforce-contract foo _ --pointer-check -^\[foo.assigns.*\d+\].* line 8 Check that x\[\(.*\)1\] is assignable: (SUCCESS|FAILURE)$ -^\[foo.assigns.*\d+\].* line 8 Check that x\[\(.*\)1\] is assignable: FAILURE$ +^\[foo.assigns.*\d+\].* line 8 Check that x\[(\(.*\))?1\] is assignable: (SUCCESS|FAILURE)$ +^\[foo.assigns.*\d+\].* line 8 Check that x\[(\(.*\))?1\] is assignable: FAILURE$ ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/contracts-dfcc/assigns_enforce_structs_05/test.desc b/regression/contracts-dfcc/assigns_enforce_structs_05/test.desc index fbb81d3f3c3..823cf02c1fd 100644 --- a/regression/contracts-dfcc/assigns_enforce_structs_05/test.desc +++ b/regression/contracts-dfcc/assigns_enforce_structs_05/test.desc @@ -4,9 +4,9 @@ main.c ^EXIT=10$ ^SIGNAL=0$ ^\[f1.assigns.\d+\] line \d+ Check that p->y is assignable: FAILURE$ -^\[f1.assigns.\d+\] line \d+ Check that p->x\[\(.*\)0\] is assignable: SUCCESS$ -^\[f1.assigns.\d+\] line \d+ Check that p->x\[\(.*\)1\] is assignable: SUCCESS$ -^\[f1.assigns.\d+\] line \d+ Check that p->x\[\(.*\)2\] is assignable: SUCCESS$ +^\[f1.assigns.\d+\] line \d+ Check that p->x\[(\(.*\))?0\] is assignable: SUCCESS$ +^\[f1.assigns.\d+\] line \d+ Check that p->x\[(\(.*\))?1\] is assignable: SUCCESS$ +^\[f1.assigns.\d+\] line \d+ Check that p->x\[(\(.*\))?2\] is assignable: SUCCESS$ ^VERIFICATION FAILED$ -- -- diff --git a/regression/contracts-dfcc/assigns_enforce_structs_06/test-f1.desc b/regression/contracts-dfcc/assigns_enforce_structs_06/test-f1.desc index a0ca61df0c3..73896d10b3d 100644 --- a/regression/contracts-dfcc/assigns_enforce_structs_06/test-f1.desc +++ b/regression/contracts-dfcc/assigns_enforce_structs_06/test-f1.desc @@ -3,9 +3,9 @@ main.c --dfcc main --enforce-contract f1 ^EXIT=10$ ^SIGNAL=0$ -^\[f1.assigns.\d+\] line \d+ Check that p->buf\[\(.*\)0\] is assignable: SUCCESS$ -^\[f1.assigns.\d+\] line \d+ Check that p->buf\[\(.*\)1\] is assignable: SUCCESS$ -^\[f1.assigns.\d+\] line \d+ Check that p->buf\[\(.*\)2\] is assignable: SUCCESS$ +^\[f1.assigns.\d+\] line \d+ Check that p->buf\[(\(.*\))?0\] is assignable: SUCCESS$ +^\[f1.assigns.\d+\] line \d+ Check that p->buf\[(\(.*\))?1\] is assignable: SUCCESS$ +^\[f1.assigns.\d+\] line \d+ Check that p->buf\[(\(.*\))?2\] is assignable: SUCCESS$ ^\[f1.assigns.\d+\] line \d+ Check that p->size is assignable: FAILURE$ ^VERIFICATION FAILED$ -- diff --git a/regression/contracts-dfcc/assigns_enforce_structs_06/test-f2.desc b/regression/contracts-dfcc/assigns_enforce_structs_06/test-f2.desc index 6a58247dbd4..779e626fd9b 100644 --- a/regression/contracts-dfcc/assigns_enforce_structs_06/test-f2.desc +++ b/regression/contracts-dfcc/assigns_enforce_structs_06/test-f2.desc @@ -3,7 +3,7 @@ main.c --dfcc main --enforce-contract f2 ^EXIT=10$ ^SIGNAL=0$ -^\[f2.assigns.\d+\] line \d+ Check that p->buf\[\(.*\)0\] is assignable: FAILURE$ +^\[f2.assigns.\d+\] line \d+ Check that p->buf\[(\(.*\))?0\] is assignable: FAILURE$ ^\[f2.assigns.\d+\] line \d+ Check that p->size is assignable: SUCCESS$ ^VERIFICATION FAILED$ -- diff --git a/regression/contracts-dfcc/assigns_enforce_structs_07/test-f1.desc b/regression/contracts-dfcc/assigns_enforce_structs_07/test-f1.desc index 48ee2f48940..213ac15db57 100644 --- a/regression/contracts-dfcc/assigns_enforce_structs_07/test-f1.desc +++ b/regression/contracts-dfcc/assigns_enforce_structs_07/test-f1.desc @@ -3,7 +3,7 @@ main.c --malloc-may-fail --malloc-fail-null --dfcc main --enforce-contract f1 _ --pointer-check ^EXIT=10$ ^SIGNAL=0$ -^\[f1.assigns.\d+\].*line 18 Check that p->buf\[\(.*\)0\] is assignable: FAILURE$ +^\[f1.assigns.\d+\].*line 18 Check that p->buf\[(\(.*\))?0\] is assignable: FAILURE$ ^VERIFICATION FAILED$ -- -- diff --git a/regression/contracts-dfcc/assigns_enforce_structs_07/test-f2.desc b/regression/contracts-dfcc/assigns_enforce_structs_07/test-f2.desc index a0ebcd86895..152ddbc55bd 100644 --- a/regression/contracts-dfcc/assigns_enforce_structs_07/test-f2.desc +++ b/regression/contracts-dfcc/assigns_enforce_structs_07/test-f2.desc @@ -3,7 +3,7 @@ main.c --malloc-may-fail --malloc-fail-null --dfcc main --enforce-contract f2 _ --pointer-check ^EXIT=10$ ^SIGNAL=0$ -^\[f2.assigns.\d+\].*line 23 Check that pp->p->buf\[\(.*\)0\] is assignable: FAILURE$ +^\[f2.assigns.\d+\].*line 23 Check that pp->p->buf\[(\(.*\))?0\] is assignable: FAILURE$ ^VERIFICATION FAILED$ -- -- diff --git a/regression/contracts-dfcc/assigns_enforce_structs_08/test-f1.desc b/regression/contracts-dfcc/assigns_enforce_structs_08/test-f1.desc index ae4d709b2fe..0da49818db0 100644 --- a/regression/contracts-dfcc/assigns_enforce_structs_08/test-f1.desc +++ b/regression/contracts-dfcc/assigns_enforce_structs_08/test-f1.desc @@ -1,7 +1,7 @@ CORE dfcc-only main.c --dfcc main --enforce-contract f1 _ --malloc-may-fail --malloc-fail-null --pointer-check -^\[f1.assigns.\d+\] line \d+ Check that p->buf\[\(.*\)0\] is assignable: SUCCESS$ +^\[f1.assigns.\d+\] line \d+ Check that p->buf\[(\(.*\))?0\] is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/contracts-dfcc/assigns_enforce_structs_08/test-f2.desc b/regression/contracts-dfcc/assigns_enforce_structs_08/test-f2.desc index 81632e6070c..cb4bc489c36 100644 --- a/regression/contracts-dfcc/assigns_enforce_structs_08/test-f2.desc +++ b/regression/contracts-dfcc/assigns_enforce_structs_08/test-f2.desc @@ -1,7 +1,7 @@ CORE dfcc-only main.c --dfcc main --enforce-contract f2 _ --malloc-may-fail --malloc-fail-null --pointer-check -^\[f2.assigns.\d+\] line \d+ Check that pp->p->buf\[\(.*\)0\] is assignable: SUCCESS$ +^\[f2.assigns.\d+\] line \d+ Check that pp->p->buf\[(\(.*\))?0\] is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/contracts-dfcc/assigns_type_checking_valid_cases/test-foo8.desc b/regression/contracts-dfcc/assigns_type_checking_valid_cases/test-foo8.desc index 21d30e188ac..51d241a90ed 100644 --- a/regression/contracts-dfcc/assigns_type_checking_valid_cases/test-foo8.desc +++ b/regression/contracts-dfcc/assigns_type_checking_valid_cases/test-foo8.desc @@ -3,16 +3,16 @@ main.c --dfcc main --enforce-contract foo8 _ --pointer-primitive-check ^EXIT=0$ ^SIGNAL=0$ -^\[foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)0\] is assignable: SUCCESS$ -^\[foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)1\] is assignable: SUCCESS$ -^\[foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)2\] is assignable: SUCCESS$ -^\[foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)3\] is assignable: SUCCESS$ -^\[foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)4\] is assignable: SUCCESS$ -^\[foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)5\] is assignable: SUCCESS$ -^\[foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)6\] is assignable: SUCCESS$ -^\[foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)7\] is assignable: SUCCESS$ -^\[foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)8\] is assignable: SUCCESS$ -^\[foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)9\] is assignable: SUCCESS$ +^\[foo8.assigns.\d+\] line \d+ Check that array\[(\(.* int\))?0\] is assignable: SUCCESS$ +^\[foo8.assigns.\d+\] line \d+ Check that array\[(\(.* int\))?1\] is assignable: SUCCESS$ +^\[foo8.assigns.\d+\] line \d+ Check that array\[(\(.* int\))?2\] is assignable: SUCCESS$ +^\[foo8.assigns.\d+\] line \d+ Check that array\[(\(.* int\))?3\] is assignable: SUCCESS$ +^\[foo8.assigns.\d+\] line \d+ Check that array\[(\(.* int\))?4\] is assignable: SUCCESS$ +^\[foo8.assigns.\d+\] line \d+ Check that array\[(\(.* int\))?5\] is assignable: SUCCESS$ +^\[foo8.assigns.\d+\] line \d+ Check that array\[(\(.* int\))?6\] is assignable: SUCCESS$ +^\[foo8.assigns.\d+\] line \d+ Check that array\[(\(.* int\))?7\] is assignable: SUCCESS$ +^\[foo8.assigns.\d+\] line \d+ Check that array\[(\(.* int\))?8\] is assignable: SUCCESS$ +^\[foo8.assigns.\d+\] line \d+ Check that array\[(\(.* int\))?9\] is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- Checks whether CBMC parses correctly all standard cases for assigns clauses. diff --git a/regression/contracts-dfcc/invar_havoc_dynamic_array/test.desc b/regression/contracts-dfcc/invar_havoc_dynamic_array/test.desc index e0d6bbf766c..3b81537a6a2 100644 --- a/regression/contracts-dfcc/invar_havoc_dynamic_array/test.desc +++ b/regression/contracts-dfcc/invar_havoc_dynamic_array/test.desc @@ -8,7 +8,7 @@ main.c ^\[main.loop_invariant_step.\d+\] line 11 Check invariant after step for loop .*: SUCCESS$ ^\[main.loop_step_unwinding.\d+\] line 11 Check step was unwound for loop .*: SUCCESS$ ^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ -^\[main.assigns.\d+\] .* Check that data\[\(signed long (long )?int\)i\] is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that data\[(\(signed (long (long )?)?int\))?i\] is assignable: SUCCESS$ ^\[main\.assertion\.\d+\] .* assertion data\[5\] == 0: FAILURE$ ^\[main\.assertion\.\d+\] .* assertion data\[5\] == 1: FAILURE$ ^VERIFICATION FAILED$ diff --git a/regression/contracts-dfcc/invar_havoc_dynamic_array_const_idx/test.desc b/regression/contracts-dfcc/invar_havoc_dynamic_array_const_idx/test.desc index 45c7baa0489..7bdd98b3675 100644 --- a/regression/contracts-dfcc/invar_havoc_dynamic_array_const_idx/test.desc +++ b/regression/contracts-dfcc/invar_havoc_dynamic_array_const_idx/test.desc @@ -8,7 +8,7 @@ main.c ^\[main.loop_invariant_step.\d+\] line 12 Check invariant after step for loop .*: SUCCESS$ ^\[main.loop_step_unwinding.\d+\] line 12 Check step was unwound for loop .*: SUCCESS$ ^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ -^\[main.assigns.\d+\] .* Check that data\[\(signed long (long )?int\)1\] is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that data\[(\(signed (long (long )?)?int\))?1\] is assignable: SUCCESS$ ^\[main\.assertion\.\d+\] .* assertion data\[1\] == 0 \|\| data\[1\] == 1: FAILURE$ ^\[main\.assertion\.\d+\] .* assertion data\[4\] == 0: SUCCESS$ ^VERIFICATION FAILED$ diff --git a/regression/contracts-dfcc/invar_havoc_static_array/test.desc b/regression/contracts-dfcc/invar_havoc_static_array/test.desc index 4f49c1e7f5e..d4b64690d42 100644 --- a/regression/contracts-dfcc/invar_havoc_static_array/test.desc +++ b/regression/contracts-dfcc/invar_havoc_static_array/test.desc @@ -8,7 +8,7 @@ main.c ^\[main.loop_invariant_step.\d+\] line 11 Check invariant after step for loop .*: SUCCESS$ ^\[main.loop_step_unwinding.\d+\] line 11 Check step was unwound for loop .*: SUCCESS$ ^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ -^\[main.assigns.\d+\] .* Check that data\[\(signed long (long )?int\)i\] is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that data\[(\(signed (long (long )?)?int\))?i\] is assignable: SUCCESS$ ^\[main\.assertion\.\d+\] .* assertion data\[5\] == 0: FAILURE$ ^\[main\.assertion\.\d+\] .* assertion data\[5\] == 1: FAILURE$ ^VERIFICATION FAILED$ diff --git a/regression/contracts-dfcc/invar_havoc_static_array_const_idx/test.desc b/regression/contracts-dfcc/invar_havoc_static_array_const_idx/test.desc index 303ea1596e1..c91d92eeaaf 100644 --- a/regression/contracts-dfcc/invar_havoc_static_array_const_idx/test.desc +++ b/regression/contracts-dfcc/invar_havoc_static_array_const_idx/test.desc @@ -8,7 +8,7 @@ main.c ^\[main.loop_invariant_step.\d+\] line 12 Check invariant after step for loop .*: SUCCESS$ ^\[main.loop_step_unwinding.\d+\] line 12 Check step was unwound for loop .*: SUCCESS$ ^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ -^\[main.assigns.\d+\] .* Check that data\[\(signed long (long )?int\)1\] is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that data\[(\(signed (long (long )?)?int\))?1\] is assignable: SUCCESS$ ^\[main\.assertion\.\d+\] .* assertion data\[1\] == 0 \|\| data\[1\] == 1: FAILURE$ ^\[main\.assertion\.\d+\] .* assertion data\[4\] == 0: SUCCESS$ ^VERIFICATION FAILED$ diff --git a/regression/contracts-dfcc/invar_havoc_static_multi-dim_array_all_const_idx/test.desc b/regression/contracts-dfcc/invar_havoc_static_multi-dim_array_all_const_idx/test.desc index a94daab6908..a1bf2967d78 100644 --- a/regression/contracts-dfcc/invar_havoc_static_multi-dim_array_all_const_idx/test.desc +++ b/regression/contracts-dfcc/invar_havoc_static_multi-dim_array_all_const_idx/test.desc @@ -7,7 +7,7 @@ main.c ^\[main.loop_invariant_base.\d+\] line 13 Check invariant before entry for loop .*: SUCCESS$ ^\[main.loop_invariant_step.\d+\] line 13 Check invariant after step for loop .*: SUCCESS$ ^\[main.loop_step_unwinding.\d+\] line 13 Check step was unwound for loop .*: SUCCESS$ -^\[main.assigns.\d+\] .* Check that data\[\(signed long (long )?int\)4\]\[\(signed long (long )?int\)5\]\[\(signed long (long )?int\)6\] is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that data\[(\(signed long (long )?int\))?4\]\[(\(signed long (long )?int\))?5\]\[(\(signed long (long )?int\))?6\] is assignable: SUCCESS$ ^\[main\.assertion\.\d+\] .* assertion data\[4\]\[5\]\[6\] == 0: FAILURE$ ^\[main\.assertion\.\d+\] .* assertion data\[1\]\[2\]\[3\] == 0: SUCCESS$ ^VERIFICATION FAILED$ diff --git a/regression/contracts-dfcc/invar_havoc_static_multi-dim_array_partial_const_idx/test.desc b/regression/contracts-dfcc/invar_havoc_static_multi-dim_array_partial_const_idx/test.desc index 96a251f3471..91550624be0 100644 --- a/regression/contracts-dfcc/invar_havoc_static_multi-dim_array_partial_const_idx/test.desc +++ b/regression/contracts-dfcc/invar_havoc_static_multi-dim_array_partial_const_idx/test.desc @@ -8,7 +8,7 @@ main.c ^\[main.loop_invariant_step.\d+\] line 13 Check invariant after step for loop .*: SUCCESS$ ^\[main.loop_step_unwinding.\d+\] line 13 Check step was unwound for loop .*: SUCCESS$ ^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ -^\[main.assigns.\d+\] .* Check that data\[\(signed long (long )?int\)4\]\[\(signed long (long )?int\)i\]\[\(signed long (long )?int\)6\] is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that data\[(\(signed long (long )?int\))?4\]\[(\(signed (long (long )?)?int\))?i\]\[(\(signed long (long )?int\))?6\] is assignable: SUCCESS$ ^\[main\.assertion\.\d+\] .* assertion data\[1\]\[2\]\[3\] == 0: FAILURE$ ^\[main\.assertion\.\d+\] .* assertion data\[4\]\[5\]\[6\] == 0: FAILURE$ ^VERIFICATION FAILED$ diff --git a/regression/contracts-dfcc/loop-freeness-check/test.desc b/regression/contracts-dfcc/loop-freeness-check/test.desc index ef93e2830c9..a018f665fae 100644 --- a/regression/contracts-dfcc/loop-freeness-check/test.desc +++ b/regression/contracts-dfcc/loop-freeness-check/test.desc @@ -2,7 +2,7 @@ CORE dfcc-only main.c --dfcc main --enforce-contract foo ^\[foo.assigns.\d+\].*Check that i is assignable: SUCCESS$ -^\[foo.assigns.\d+\].*Check that arr\[\(.*\)i\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\].*Check that arr\[(\(.*\))?i\] is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/contracts-dfcc/loop_assigns-slice-assignable-scalar/test.desc b/regression/contracts-dfcc/loop_assigns-slice-assignable-scalar/test.desc index 65b6121277f..9735a8dcd79 100644 --- a/regression/contracts-dfcc/loop_assigns-slice-assignable-scalar/test.desc +++ b/regression/contracts-dfcc/loop_assigns-slice-assignable-scalar/test.desc @@ -8,8 +8,8 @@ main.c ^\[main.loop_invariant_step.\d+\] line 21 Check invariant after step for loop .*: SUCCESS$ ^\[main.loop_step_unwinding.\d+\] line 21 Check step was unwound for loop .*: SUCCESS$ ^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ -^\[main.assigns.\d+\] .* Check that b->data\[\(.*\)0\] is assignable: SUCCESS$ -^\[main.assigns.\d+\] .* Check that b->data\[\(.*\)i\] is assignable: FAILURE$ +^\[main.assigns.\d+\] .* Check that b->data\[(\(.*\))?0\] is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that b->data\[(\(.*\))?i\] is assignable: FAILURE$ ^\[main.assertion.\d+\] .* assertion b->data\[0\] == 0: FAILURE$ ^\[main.assertion.\d+\] .* assertion b->data\[1\] == 0: SUCCESS$ ^\[main.assertion.\d+\] .* assertion b->data\[2\] == 0: SUCCESS$ diff --git a/regression/contracts-dfcc/loop_assigns-slice-upto-fail/test.desc b/regression/contracts-dfcc/loop_assigns-slice-upto-fail/test.desc index 06cd5cef0e7..37d8ece603e 100644 --- a/regression/contracts-dfcc/loop_assigns-slice-upto-fail/test.desc +++ b/regression/contracts-dfcc/loop_assigns-slice-upto-fail/test.desc @@ -6,10 +6,10 @@ main.c ^\[main.loop_invariant_step.\d+\] line 21 Check invariant after step for loop .*: SUCCESS$ ^\[main.loop_step_unwinding.\d+\] line 21 Check step was unwound for loop .*: SUCCESS$ ^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ -^\[main.assigns.\d+\] .* Check that b->data\[\(.*\)0\] is assignable: SUCCESS$ -^\[main.assigns.\d+\] .* Check that b->data\[\(.*\)1\] is assignable: SUCCESS$ -^\[main.assigns.\d+\] .* Check that b->data\[\(.*\)2\] is assignable: SUCCESS$ -^\[main.assigns.\d+\] .* Check that b->data\[\(.*\)i\] is assignable: FAILURE$ +^\[main.assigns.\d+\] .* Check that b->data\[(\(.*\))?0\] is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that b->data\[(\(.*\))?1\] is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that b->data\[(\(.*\))?2\] is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that b->data\[(\(.*\))?i\] is assignable: FAILURE$ ^\[main.assertion.\d+\] .* assertion b->data\[0\] == 0: FAILURE$ ^\[main.assertion.\d+\] .* assertion b->data\[1\] == 0: FAILURE$ ^\[main.assertion.\d+\] .* assertion b->data\[2\] == 0: FAILURE$ diff --git a/regression/contracts-dfcc/loop_assigns_target_base_idents/test.desc b/regression/contracts-dfcc/loop_assigns_target_base_idents/test.desc index 682eb3bd093..4ffacfd2309 100644 --- a/regression/contracts-dfcc/loop_assigns_target_base_idents/test.desc +++ b/regression/contracts-dfcc/loop_assigns_target_base_idents/test.desc @@ -6,17 +6,17 @@ main.c ^\[foo.loop_invariant_base.\d+\] line .* Check invariant before entry for loop foo.0: SUCCESS$ ^\[foo.loop_invariant_step.\d+\] line .* Check invariant after step for loop foo.0: SUCCESS$ ^\[foo.loop_step_unwinding.\d+\] line .* Check step was unwound for loop foo.0: SUCCESS$ -^\[foo.assigns.\d+\] line .* Check that buf1\[\(.*\)i\] is assignable: SUCCESS$ -^\[foo.assigns.\d+\] line .* Check that buf1\[\(.*\)\(32 - 1\)\] is assignable: SUCCESS$ -^\[foo.assigns.\d+\] line .* Check that buf2\[\(.*\)0\] is assignable: FAILURE$ -^\[foo.assigns.\d+\] line .* Check that buf2\[\(.*\)10\] is assignable: SUCCESS$ -^\[foo.assigns.\d+\] line .* Check that buf2\[\(.*\)11\] is assignable: SUCCESS$ -^\[foo.assigns.\d+\] line .* Check that buf1\[\(.*\)\(32 - 1\)\] is assignable: SUCCESS$ -^\[foo.assigns.\d+\] line .* Check that buf3\[\(.*\)0\] is assignable: FAILURE$ -^\[foo.assigns.\d+\] line .* Check that buf3\[\(.*\)9\] is assignable: FAILURE$ -^\[foo.assigns.\d+\] line .* Check that buf3\[\(.*\)10\] is assignable: SUCCESS$ -^\[foo.assigns.\d+\] line .* Check that buf3\[\(.*\)11\] is assignable: FAILURE$ -^\[foo.assigns.\d+\] line .* Check that buf3\[\(.*\)\(32 - 1\)\] is assignable: FAILURE$ +^\[foo.assigns.\d+\] line .* Check that buf1\[(\(.*\))?i\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line .* Check that buf1\[(\(.*\))?\(?32 - 1\)?\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line .* Check that buf2\[(\(.*\))?0\] is assignable: FAILURE$ +^\[foo.assigns.\d+\] line .* Check that buf2\[(\(.*\))?10\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line .* Check that buf2\[(\(.*\))?11\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line .* Check that buf1\[(\(.*\))?\(?32 - 1\)?\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line .* Check that buf3\[(\(.*\))?0\] is assignable: FAILURE$ +^\[foo.assigns.\d+\] line .* Check that buf3\[(\(.*\))?9\] is assignable: FAILURE$ +^\[foo.assigns.\d+\] line .* Check that buf3\[(\(.*\))?10\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line .* Check that buf3\[(\(.*\))?11\] is assignable: FAILURE$ +^\[foo.assigns.\d+\] line .* Check that buf3\[(\(.*\))?\(?32 - 1\)?\] is assignable: FAILURE$ ^\[foo.assigns.\d+\] line .* Check that i is assignable: SUCCESS$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/contracts-dfcc/loop_contracts_binary_search/main.c b/regression/contracts-dfcc/loop_contracts_binary_search/main.c index 18a3cd67ff3..deaf50081f5 100644 --- a/regression/contracts-dfcc/loop_contracts_binary_search/main.c +++ b/regression/contracts-dfcc/loop_contracts_binary_search/main.c @@ -32,7 +32,8 @@ int binary_search(int val, int *buf, int size) int main() { - int val, size; + int val; + char size; int *buf = size >= 0 ? malloc(size * sizeof(int)) : NULL; int idx = binary_search(val, buf, size); diff --git a/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-assert-bounded.desc b/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-assert-bounded.desc index 173445e6b92..3bcea68d4a5 100644 --- a/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-assert-bounded.desc +++ b/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-assert-bounded.desc @@ -6,11 +6,11 @@ main_bounded.c ^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ ptr NULL or writable up to size: SUCCESS$ ^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ no offset bits overflow on CAR upper bound computation: SUCCESS$ ^\[foo.assertion.\d+\] line \d+ size is capped: SUCCESS$ -^\[foo.assigns.\d+\] line \d+ Check that arr\[\(.*\)0\] is assignable: SUCCESS$ -^\[foo.assigns.\d+\] line \d+ Check that arr\[\(.*\)\(size - \(.*\)1\)\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line \d+ Check that arr\[(\(.*\))?0\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line \d+ Check that arr\[(\(.*\))?\(size - \(.*\)1\)\] is assignable: SUCCESS$ ^\[foo.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): SUCCESS$ ^\[foo.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): SUCCESS$ -^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[\(.*\)\(size - \(.*\)1\)\]: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[(\(.*\))?\(size - \(.*\)1\)\]: SUCCESS$ ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-assert.desc b/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-assert.desc index 7c20dc70831..ac59da14194 100644 --- a/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-assert.desc +++ b/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-assert.desc @@ -6,11 +6,11 @@ main.c ^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ ptr NULL or writable up to size: SUCCESS$ ^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ no offset bits overflow on CAR upper bound computation: SUCCESS$ ^\[foo.assertion.\d+\] line \d+ size is capped: SUCCESS$ -^\[foo.assigns.\d+\] line \d+ Check that arr\[\(.*\)0\] is assignable: SUCCESS$ -^\[foo.assigns.\d+\] line \d+ Check that arr\[\(.*\)\(size - \(.*\)1\)\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line \d+ Check that arr\[(\(.*\))?0\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line \d+ Check that arr\[(\(.*\))?\(size - \(.*\)1\)\] is assignable: SUCCESS$ ^\[foo.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): SUCCESS$ ^\[foo.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): SUCCESS$ -^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[\(.*\)\(size - \(.*\)1\)\]: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[(\(.*\))?\(size - \(.*\)1\)\]: SUCCESS$ ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-none-bounded.desc b/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-none-bounded.desc index 9788d6bae1a..57f770674bf 100644 --- a/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-none-bounded.desc +++ b/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-none-bounded.desc @@ -5,11 +5,11 @@ main_bounded.c ^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ ptr NULL or writable up to size: SUCCESS$ ^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ no offset bits overflow on CAR upper bound computation: SUCCESS$ ^\[foo.assertion.\d+\] line \d+ size is capped: SUCCESS$ -^\[foo.assigns.\d+\] line \d+ Check that arr\[\(.*\)0\] is assignable: SUCCESS$ -^\[foo.assigns.\d+\] line \d+ Check that arr\[\(.*\)\(size - \(.*\)1\)\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line \d+ Check that arr\[(\(.*\))?0\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line \d+ Check that arr\[(\(.*\))?\(size - \(.*\)1\)\] is assignable: SUCCESS$ ^\[foo.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): SUCCESS$ ^\[foo.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): SUCCESS$ -^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[\(.*\)\(size - \(.*\)1\)\]: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[(\(.*\))?\(size - \(.*\)1\)\]: SUCCESS$ ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-null-bounded.desc b/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-null-bounded.desc index 1f0bb2c9e7e..c205e6848ec 100644 --- a/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-null-bounded.desc +++ b/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-null-bounded.desc @@ -5,11 +5,11 @@ main_bounded.c ^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ ptr NULL or writable up to size: SUCCESS$ ^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ no offset bits overflow on CAR upper bound computation: SUCCESS$ ^\[foo.assertion.\d+\] line \d+ size is capped: SUCCESS$ -^\[foo.assigns.\d+\] line \d+ Check that arr\[\(.*\)0\] is assignable: SUCCESS$ -^\[foo.assigns.\d+\] line \d+ Check that arr\[\(.*\)\(size - \(.*\)1\)\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line \d+ Check that arr\[(\(.*\))?0\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line \d+ Check that arr\[(\(.*\))?\(size - \(.*\)1\)\] is assignable: SUCCESS$ ^\[foo.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): SUCCESS$ ^\[foo.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): SUCCESS$ -^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[\(.*\)\(size - \(.*\)1\)\]: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[(\(.*\))?\(size - \(.*\)1\)\]: SUCCESS$ ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-null.desc b/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-null.desc index 2325a4ab7ff..b4e1d78ed77 100644 --- a/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-null.desc +++ b/regression/contracts-dfcc/memory-predicates-is-fresh-failure-modes/test-fail-null.desc @@ -5,11 +5,11 @@ main.c ^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ ptr NULL or writable up to size: SUCCESS$ ^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ no offset bits overflow on CAR upper bound computation: SUCCESS$ ^\[foo.assertion.\d+\] line \d+ size is capped: SUCCESS$ -^\[foo.assigns.\d+\] line \d+ Check that arr\[\(.*\)0\] is assignable: SUCCESS$ -^\[foo.assigns.\d+\] line \d+ Check that arr\[\(.*\)\(size - \(.*\)1\)\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line \d+ Check that arr\[(\(.*\))?0\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line \d+ Check that arr\[(\(.*\))?\(size - \(.*\)1\)\] is assignable: SUCCESS$ ^\[foo.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): SUCCESS$ ^\[foo.pointer_arithmetic.\d+\] line \d+ pointer arithmetic: pointer outside object bounds in arr \+ \(.*\)\(size - \(.*\)1\): SUCCESS$ -^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[\(.*\)\(size - \(.*\)1\)\]: SUCCESS$ +^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[(\(.*\))?\(size - \(.*\)1\)\]: SUCCESS$ ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/contracts-dfcc/quantifiers-forall-ensures-enforce/test.desc b/regression/contracts-dfcc/quantifiers-forall-ensures-enforce/test.desc index 8458deb6fd9..456d05de164 100644 --- a/regression/contracts-dfcc/quantifiers-forall-ensures-enforce/test.desc +++ b/regression/contracts-dfcc/quantifiers-forall-ensures-enforce/test.desc @@ -4,11 +4,11 @@ main.c ^EXIT=0$ ^SIGNAL=0$ ^\[f1.postcondition.\d+\] line \d+ Check ensures clause of contract contract::f1 for function f1: SUCCESS$ -^\[f1.assigns.\d+\] line \d+ Check that arr\[\(.*\)\d\] is assignable: SUCCESS$ +^\[f1.assigns.\d+\] line \d+ Check that arr\[(\(.*\))?\d\] is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- ^warning: ignoring -^\[f1.assigns.\d+\] line \d+ Check that arr\[\(.*\)\d\] is assignable: FAILURE$ +^\[f1.assigns.\d+\] line \d+ Check that arr\[(\(.*\))?\d\] is assignable: FAILURE$ -- The purpose of this test is to ensure that we can safely use __CPROVER_forall within positive contexts (enforced ENSURES clauses). diff --git a/regression/contracts-dfcc/quantifiers-loop-01/test.desc b/regression/contracts-dfcc/quantifiers-loop-01/test.desc index 29c882f55b1..1250d24d25b 100644 --- a/regression/contracts-dfcc/quantifiers-loop-01/test.desc +++ b/regression/contracts-dfcc/quantifiers-loop-01/test.desc @@ -6,7 +6,7 @@ main.c ^\[main.loop_invariant_step.\d+\] line 10 Check invariant after step for loop .*: SUCCESS$ ^\[main.loop_step_unwinding.\d+\] line 10 Check step was unwound for loop .*: SUCCESS$ ^\[main.assigns.\d+\] line .* Check that i is assignable: SUCCESS$ -^\[main.assigns.\d+\] line .* Check that a\[\(signed long (long )?int\)i\] is assignable: SUCCESS$ +^\[main.assigns.\d+\] line .* Check that a\[(\(signed (long (long )?)?int\))?i\] is assignable: SUCCESS$ ^\[main\.assertion\.\d+\] line .* assertion a\[10\] == 1: SUCCESS$ ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ diff --git a/regression/contracts-dfcc/quantifiers-loop-02/test.desc b/regression/contracts-dfcc/quantifiers-loop-02/test.desc index 57e027c8708..23c3147f616 100644 --- a/regression/contracts-dfcc/quantifiers-loop-02/test.desc +++ b/regression/contracts-dfcc/quantifiers-loop-02/test.desc @@ -10,7 +10,7 @@ main.c ^\[main.loop_invariant_step.\d+\] line 9 Check invariant after step for loop .*: SUCCESS$ ^\[main.loop_step_unwinding.\d+\] line 9 Check step was unwound for loop .*: SUCCESS$ ^\[main.assigns.\d+\] line .* Check that i is assignable: SUCCESS$ -^\[main.assigns.\d+\] line .* Check that a\[\(signed long (long )?int\)i\] is assignable: SUCCESS$ +^\[main.assigns.\d+\] line .* Check that a\[(\(signed (long (long )?)?int\))?i\] is assignable: SUCCESS$ ^\[main.assertion.\d+\] line .* assertion .*: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- diff --git a/regression/contracts-dfcc/quantifiers-loop-03/test.desc b/regression/contracts-dfcc/quantifiers-loop-03/test.desc index e71da9dd258..c577bcb4cd0 100644 --- a/regression/contracts-dfcc/quantifiers-loop-03/test.desc +++ b/regression/contracts-dfcc/quantifiers-loop-03/test.desc @@ -8,7 +8,7 @@ main.c ^\[main.loop_invariant_step.\d+\] line 13 Check invariant after step for loop .*: SUCCESS$ ^\[main.loop_step_unwinding.\d+\] line 13 Check step was unwound for loop .*: SUCCESS$ ^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ -^\[main.assigns.\d+\] .* Check that a\[\(signed long (long )?int\)i\] is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that a\[(\(signed (long (long )?)?int\))?i\] is assignable: SUCCESS$ ^\[main\.assertion\.\d+\] line .* assertion .*: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- diff --git a/regression/contracts-dfcc/test_array_memory_enforce/test.desc b/regression/contracts-dfcc/test_array_memory_enforce/test.desc index 3ed2e82468f..fd61c6766d7 100644 --- a/regression/contracts-dfcc/test_array_memory_enforce/test.desc +++ b/regression/contracts-dfcc/test_array_memory_enforce/test.desc @@ -5,8 +5,8 @@ main.c ^SIGNAL=0$ \[foo.postcondition.\d+\] line \d+ Check ensures clause( of contract contract::foo for function foo)?: SUCCESS \[foo.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS -\[foo.assigns.\d+\] line \d+ Check that x\[\(.* int\)5\] is assignable: SUCCESS -\[foo.assigns.\d+\] line \d+ Check that x\[\(.* int\)9\] is assignable: SUCCESS +\[foo.assigns.\d+\] line \d+ Check that x\[(\(.* int\))?5\] is assignable: SUCCESS +\[foo.assigns.\d+\] line \d+ Check that x\[(\(.* int\))?9\] is assignable: SUCCESS ^VERIFICATION SUCCESSFUL$ -- -- diff --git a/regression/contracts-dfcc/test_struct_member_enforce/test.desc b/regression/contracts-dfcc/test_struct_member_enforce/test.desc index 5c1636b03be..cb6c118fb10 100644 --- a/regression/contracts-dfcc/test_struct_member_enforce/test.desc +++ b/regression/contracts-dfcc/test_struct_member_enforce/test.desc @@ -4,7 +4,7 @@ main.c ^EXIT=0$ ^SIGNAL=0$ \[foo.postcondition.\d+\] line \d+ Check ensures clause( of contract contract::foo for function foo)?: SUCCESS$ -\[foo.assigns.\d+\] line \d+ Check that x->str\[\(.*\)\(x->len - 1\)\] is assignable: SUCCESS +\[foo.assigns.\d+\] line \d+ Check that x->str\[(\(.*\))?\(?x->len - 1\)?\] is assignable: SUCCESS \[main.assertion.\d+\] line \d+ assertion rval \=\= 128: SUCCESS ^VERIFICATION SUCCESSFUL$ -- diff --git a/regression/contracts/assigns-enforce-malloc-zero/test.desc b/regression/contracts/assigns-enforce-malloc-zero/test.desc index 43dcf8ef277..1f9594df2fd 100644 --- a/regression/contracts/assigns-enforce-malloc-zero/test.desc +++ b/regression/contracts/assigns-enforce-malloc-zero/test.desc @@ -2,7 +2,7 @@ CORE main.c --enforce-contract foo _ --malloc-may-fail --malloc-fail-null ^\[foo.assigns.\d+\] line 9 Check that __CPROVER_object_whole\(\(.* \*\)a\) is valid when a != \(\(.* \*\)NULL\): SUCCESS$ -^\[foo.assigns.\d+\] line 19 Check that a\[\(signed long (long )?int\)i\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line 19 Check that a\[(\(signed long (long )?int\))?i\] is assignable: SUCCESS$ ^EXIT=0$ ^SIGNAL=0$ ^VERIFICATION SUCCESSFUL$ diff --git a/regression/contracts/assigns-replace-malloc-zero/main.c b/regression/contracts/assigns-replace-malloc-zero/main.c index 444b33ce29f..bea3beebd27 100644 --- a/regression/contracts/assigns-replace-malloc-zero/main.c +++ b/regression/contracts/assigns-replace-malloc-zero/main.c @@ -8,7 +8,8 @@ __CPROVER_requires(0 <= size && size <= __CPROVER_max_malloc_size) __CPROVER_requires(a == NULL || __CPROVER_rw_ok(a, size)) __CPROVER_assigns(__CPROVER_object_whole(a)) __CPROVER_ensures( - a && __CPROVER_return_value >= 0 ==> a[__CPROVER_return_value] == 0) + a && __CPROVER_return_value >= 0 ==> + (__CPROVER_return_value < size && a[__CPROVER_return_value] == 0)) // clang-format on { if(!a) diff --git a/regression/contracts/assigns-replace-malloc-zero/test.desc b/regression/contracts/assigns-replace-malloc-zero/test.desc index 3aed45563ee..ceacd9b59be 100644 --- a/regression/contracts/assigns-replace-malloc-zero/test.desc +++ b/regression/contracts/assigns-replace-malloc-zero/test.desc @@ -4,7 +4,7 @@ main.c ^\[foo.precondition.\d+\] line \d+ Check requires clause of foo in main: SUCCESS$ ^EXIT=0$ ^SIGNAL=0$ -\[main\.assertion\.1\] line 35 expecting SUCCESS: SUCCESS$ +\[main\.assertion\.1\] line 36 expecting SUCCESS: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- This test checks that objects of size zero or of __CPROVER_max_malloc_size diff --git a/regression/contracts/assigns_enforce_arrays_05/test.desc b/regression/contracts/assigns_enforce_arrays_05/test.desc index 54d643ef138..2300167e82e 100644 --- a/regression/contracts/assigns_enforce_arrays_05/test.desc +++ b/regression/contracts/assigns_enforce_arrays_05/test.desc @@ -1,7 +1,7 @@ CORE main.c --enforce-contract uses_assigns -^\[uses_assigns.assigns.\d+\] line \d+ Check that \*\(&a\[\(.*int\)i\]\) is valid: SUCCESS$ +^\[uses_assigns.assigns.\d+\] line \d+ Check that \*\(&a\[(\(.*int\))?i\]\) is valid: SUCCESS$ ^\[assigns_ptr.assigns.\d+\] line \d+ Check that \*x is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ diff --git a/regression/contracts/assigns_enforce_conditional_pointer_object/test.desc b/regression/contracts/assigns_enforce_conditional_pointer_object/test.desc index 59513d2907f..8988983d01e 100644 --- a/regression/contracts/assigns_enforce_conditional_pointer_object/test.desc +++ b/regression/contracts/assigns_enforce_conditional_pointer_object/test.desc @@ -4,12 +4,12 @@ main.c main.c function foo ^\[foo.assigns.\d+\] line 6 Check that __CPROVER_object_whole\(\(.* \*\)x\) is valid when a != FALSE: SUCCESS$ ^\[foo.assigns.\d+\] line 7 Check that __CPROVER_object_whole\(\(.* \*\)y\) is valid when !\(a != FALSE\): SUCCESS$ -^\[foo.assigns.\d+\] line 13 Check that x\[\(signed (long )?long int\)0\] is assignable: SUCCESS$ -^\[foo.assigns.\d+\] line 14 Check that y\[\(signed (long )?long int\)0\] is assignable: FAILURE$ -^\[foo.assigns.\d+\] line 18 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$ -^\[foo.assigns.\d+\] line 19 Check that y\[\(signed (long )?long int\)0\] is assignable: SUCCESS$ -^\[foo.assigns.\d+\] line 22 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$ -^\[foo.assigns.\d+\] line 23 Check that y\[\(signed (long )?long int\)0\] is assignable: FAILURE$ +^\[foo.assigns.\d+\] line 13 Check that x\[(\(signed (long )?long int\))?0\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line 14 Check that y\[(\(signed (long )?long int\))?0\] is assignable: FAILURE$ +^\[foo.assigns.\d+\] line 18 Check that x\[(\(signed (long )?long int\))?0\] is assignable: FAILURE$ +^\[foo.assigns.\d+\] line 19 Check that y\[(\(signed (long )?long int\))?0\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line 22 Check that x\[(\(signed (long )?long int\))?0\] is assignable: FAILURE$ +^\[foo.assigns.\d+\] line 23 Check that y\[(\(signed (long )?long int\))?0\] is assignable: FAILURE$ ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/contracts/assigns_enforce_conditional_pointer_object_list/test.desc b/regression/contracts/assigns_enforce_conditional_pointer_object_list/test.desc index 954c6a0cc92..3de6cfdd906 100644 --- a/regression/contracts/assigns_enforce_conditional_pointer_object_list/test.desc +++ b/regression/contracts/assigns_enforce_conditional_pointer_object_list/test.desc @@ -4,12 +4,12 @@ main.c main.c function foo ^\[foo.assigns.\d+\] line 6 Check that __CPROVER_object_whole\(\(.*\)x\) is valid when a != FALSE: SUCCESS$ ^\[foo.assigns.\d+\] line 6 Check that __CPROVER_object_whole\(\(.*\)y\) is valid when a != FALSE: SUCCESS$ -^\[foo.assigns.\d+\] line 12 Check that x\[\(signed (long )?long int\)0\] is assignable: SUCCESS$ -^\[foo.assigns.\d+\] line 13 Check that y\[\(signed (long )?long int\)0\] is assignable: SUCCESS$ -^\[foo.assigns.\d+\] line 17 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$ -^\[foo.assigns.\d+\] line 18 Check that y\[\(signed (long )?long int\)0\] is assignable: FAILURE$ -^\[foo.assigns.\d+\] line 21 Check that x\[\(signed (long )?long int\)0\] is assignable: FAILURE$ -^\[foo.assigns.\d+\] line 22 Check that y\[\(signed (long )?long int\)0\] is assignable: FAILURE$ +^\[foo.assigns.\d+\] line 12 Check that x\[(\(signed (long )?long int\))?0\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line 13 Check that y\[(\(signed (long )?long int\))?0\] is assignable: SUCCESS$ +^\[foo.assigns.\d+\] line 17 Check that x\[(\(signed (long )?long int\))?0\] is assignable: FAILURE$ +^\[foo.assigns.\d+\] line 18 Check that y\[(\(signed (long )?long int\))?0\] is assignable: FAILURE$ +^\[foo.assigns.\d+\] line 21 Check that x\[(\(signed (long )?long int\))?0\] is assignable: FAILURE$ +^\[foo.assigns.\d+\] line 22 Check that y\[(\(signed (long )?long int\))?0\] is assignable: FAILURE$ ^VERIFICATION FAILED$ ^EXIT=10$ ^SIGNAL=0$ diff --git a/regression/contracts/assigns_enforce_offsets_2/test.desc b/regression/contracts/assigns_enforce_offsets_2/test.desc index dbf3b1e0810..dcbf3130b86 100644 --- a/regression/contracts/assigns_enforce_offsets_2/test.desc +++ b/regression/contracts/assigns_enforce_offsets_2/test.desc @@ -2,8 +2,8 @@ CORE main.c --enforce-contract foo _ --pointer-check ^\[foo.assigns.*\d+\].* line 5 Check that \*x is valid: SUCCESS$ -^\[foo.assigns.*\d+\].* line 8 Check that x\[\(.*\)1\] is assignable: (SUCCESS|FAILURE)$ -^\[foo.assigns.*\d+\].* line 8 Check that x\[\(.*\)1\] is assignable: FAILURE$ +^\[foo.assigns.*\d+\].* line 8 Check that x\[(\(.*\))?1\] is assignable: (SUCCESS|FAILURE)$ +^\[foo.assigns.*\d+\].* line 8 Check that x\[(\(.*\))?1\] is assignable: FAILURE$ ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/contracts/assigns_enforce_offsets_4/test.desc b/regression/contracts/assigns_enforce_offsets_4/test.desc index a9144122d51..0c906e82d75 100644 --- a/regression/contracts/assigns_enforce_offsets_4/test.desc +++ b/regression/contracts/assigns_enforce_offsets_4/test.desc @@ -1,7 +1,7 @@ CORE main.c --enforce-contract foo _ --pointer-check -^\[foo.assigns.*\d+\].* line 5 Check that x\[\(.*\)10\] is valid: FAILURE$ +^\[foo.assigns.*\d+\].* line 5 Check that x\[(\(.*\))?10\] is valid: FAILURE$ ^EXIT=10$ ^SIGNAL=0$ ^VERIFICATION FAILED$ diff --git a/regression/contracts/assigns_enforce_structs_06/test.desc b/regression/contracts/assigns_enforce_structs_06/test.desc index 2a56bf89725..838bcce9c4e 100644 --- a/regression/contracts/assigns_enforce_structs_06/test.desc +++ b/regression/contracts/assigns_enforce_structs_06/test.desc @@ -3,11 +3,11 @@ main.c --enforce-contract f1 --enforce-contract f2 --enforce-contract f3 ^EXIT=10$ ^SIGNAL=0$ -^\[f1.assigns.\d+\] line \d+ Check that p->buf\[\(.*\)0\] is assignable: SUCCESS$ -^\[f1.assigns.\d+\] line \d+ Check that p->buf\[\(.*\)1\] is assignable: SUCCESS$ -^\[f1.assigns.\d+\] line \d+ Check that p->buf\[\(.*\)2\] is assignable: SUCCESS$ +^\[f1.assigns.\d+\] line \d+ Check that p->buf\[(\(.*\))?0\] is assignable: SUCCESS$ +^\[f1.assigns.\d+\] line \d+ Check that p->buf\[(\(.*\))?1\] is assignable: SUCCESS$ +^\[f1.assigns.\d+\] line \d+ Check that p->buf\[(\(.*\))?2\] is assignable: SUCCESS$ ^\[f1.assigns.\d+\] line \d+ Check that p->size is assignable: FAILURE$ -^\[f2.assigns.\d+\] line \d+ Check that p->buf\[\(.*\)0\] is assignable: FAILURE$ +^\[f2.assigns.\d+\] line \d+ Check that p->buf\[(\(.*\))?0\] is assignable: FAILURE$ ^\[f2.assigns.\d+\] line \d+ Check that p->size is assignable: SUCCESS$ ^\[f3.assigns.\d+\] line \d+ Check that p->buf is assignable: SUCCESS$ ^\[f3.assigns.\d+\] line \d+ Check that p->size is assignable: SUCCESS$ diff --git a/regression/contracts/assigns_enforce_structs_07/test.desc b/regression/contracts/assigns_enforce_structs_07/test.desc index c7337935f6b..e6eac9a44bc 100644 --- a/regression/contracts/assigns_enforce_structs_07/test.desc +++ b/regression/contracts/assigns_enforce_structs_07/test.desc @@ -4,9 +4,9 @@ main.c ^EXIT=10$ ^SIGNAL=0$ ^\[f1.assigns.\d+\].*line 16 Check that \*p->buf is valid: FAILURE$ -^\[f1.assigns.\d+\].*line 18 Check that p->buf\[\(.*\)0\] is assignable: FAILURE$ +^\[f1.assigns.\d+\].*line 18 Check that p->buf\[(\(.*\))?0\] is assignable: FAILURE$ ^\[f2.assigns.\d+\].*line 21 Check that \*pp->p->buf is valid: FAILURE$ -^\[f2.assigns.\d+\].*line 23 Check that pp->p->buf\[\(.*\)0\] is assignable: FAILURE$ +^\[f2.assigns.\d+\].*line 23 Check that pp->p->buf\[(\(.*\))?0\] is assignable: FAILURE$ ^VERIFICATION FAILED$ -- -- diff --git a/regression/contracts/assigns_enforce_structs_08/test.desc b/regression/contracts/assigns_enforce_structs_08/test.desc index 054a165460b..8d7da1c07fe 100644 --- a/regression/contracts/assigns_enforce_structs_08/test.desc +++ b/regression/contracts/assigns_enforce_structs_08/test.desc @@ -1,8 +1,8 @@ CORE main.c --enforce-contract f1 --enforce-contract f2 _ --malloc-may-fail --malloc-fail-null --pointer-check -^\[f1.assigns.\d+\] line \d+ Check that p->buf\[\(.*\)0\] is assignable: SUCCESS$ -^\[f2.assigns.\d+\] line \d+ Check that pp->p->buf\[\(.*\)0\] is assignable: SUCCESS$ +^\[f1.assigns.\d+\] line \d+ Check that p->buf\[(\(.*\))?0\] is assignable: SUCCESS$ +^\[f2.assigns.\d+\] line \d+ Check that pp->p->buf\[(\(.*\))?0\] is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/contracts/assigns_type_checking_valid_cases/test.desc b/regression/contracts/assigns_type_checking_valid_cases/test.desc index 588301c9ead..6f67aaef718 100644 --- a/regression/contracts/assigns_type_checking_valid_cases/test.desc +++ b/regression/contracts/assigns_type_checking_valid_cases/test.desc @@ -12,16 +12,16 @@ main.c ^\[foo6.assigns.\d+\] line \d+ Check that buffer->len is assignable: SUCCESS$ ^\[foo7.assigns.\d+\] line \d+ Check that \*buffer->data is assignable: SUCCESS$ ^\[foo7.assigns.\d+\] line \d+ Check that buffer->len is assignable: SUCCESS$ -^\[foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)0\] is assignable: SUCCESS$ -^\[foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)1\] is assignable: SUCCESS$ -^\[foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)2\] is assignable: SUCCESS$ -^\[foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)3\] is assignable: SUCCESS$ -^\[foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)4\] is assignable: SUCCESS$ -^\[foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)5\] is assignable: SUCCESS$ -^\[foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)6\] is assignable: SUCCESS$ -^\[foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)7\] is assignable: SUCCESS$ -^\[foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)8\] is assignable: SUCCESS$ -^\[foo8.assigns.\d+\] line \d+ Check that array\[\(.* int\)9\] is assignable: SUCCESS$ +^\[foo8.assigns.\d+\] line \d+ Check that array\[(\(.* int\))?0\] is assignable: SUCCESS$ +^\[foo8.assigns.\d+\] line \d+ Check that array\[(\(.* int\))?1\] is assignable: SUCCESS$ +^\[foo8.assigns.\d+\] line \d+ Check that array\[(\(.* int\))?2\] is assignable: SUCCESS$ +^\[foo8.assigns.\d+\] line \d+ Check that array\[(\(.* int\))?3\] is assignable: SUCCESS$ +^\[foo8.assigns.\d+\] line \d+ Check that array\[(\(.* int\))?4\] is assignable: SUCCESS$ +^\[foo8.assigns.\d+\] line \d+ Check that array\[(\(.* int\))?5\] is assignable: SUCCESS$ +^\[foo8.assigns.\d+\] line \d+ Check that array\[(\(.* int\))?6\] is assignable: SUCCESS$ +^\[foo8.assigns.\d+\] line \d+ Check that array\[(\(.* int\))?7\] is assignable: SUCCESS$ +^\[foo8.assigns.\d+\] line \d+ Check that array\[(\(.* int\))?8\] is assignable: SUCCESS$ +^\[foo8.assigns.\d+\] line \d+ Check that array\[(\(.* int\))?9\] is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- Checks whether CBMC parses correctly all standard cases for assigns clauses. diff --git a/regression/contracts/invar_havoc_dynamic_array/test.desc b/regression/contracts/invar_havoc_dynamic_array/test.desc index 11bf3202c59..582a93ff682 100644 --- a/regression/contracts/invar_havoc_dynamic_array/test.desc +++ b/regression/contracts/invar_havoc_dynamic_array/test.desc @@ -6,7 +6,7 @@ main.c ^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$ ^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$ ^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ -^\[main.assigns.\d+\] .* Check that data\[\(signed long (long )?int\)i\] is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that data\[(\(signed (long (long )?)?int\))?i\] is assignable: SUCCESS$ ^\[main\.assertion\.\d+\] .* assertion data\[5\] == 0: FAILURE$ ^\[main\.assertion\.\d+\] .* assertion data\[5\] == 1: FAILURE$ ^VERIFICATION FAILED$ diff --git a/regression/contracts/invar_havoc_dynamic_array_const_idx/test.desc b/regression/contracts/invar_havoc_dynamic_array_const_idx/test.desc index 6bf09ab0360..c970e1f49b1 100644 --- a/regression/contracts/invar_havoc_dynamic_array_const_idx/test.desc +++ b/regression/contracts/invar_havoc_dynamic_array_const_idx/test.desc @@ -6,7 +6,7 @@ main.c ^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$ ^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$ ^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ -^\[main.assigns.\d+\] .* Check that data\[\(signed long (long )?int\)1\] is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that data\[(\(signed long (long )?int\))?1\] is assignable: SUCCESS$ ^\[main\.assertion\.\d+\] .* assertion data\[1\] == 0 \|\| data\[1\] == 1: FAILURE$ ^\[main\.assertion\.\d+\] .* assertion data\[4\] == 0: SUCCESS$ ^VERIFICATION FAILED$ diff --git a/regression/contracts/invar_havoc_static_array/test.desc b/regression/contracts/invar_havoc_static_array/test.desc index ced29fb215b..58e09285498 100644 --- a/regression/contracts/invar_havoc_static_array/test.desc +++ b/regression/contracts/invar_havoc_static_array/test.desc @@ -6,7 +6,7 @@ main.c ^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$ ^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$ ^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ -^\[main.assigns.\d+\] .* Check that data\[\(signed long (long )?int\)i\] is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that data\[(\(signed (long (long )?)?int\))?i\] is assignable: SUCCESS$ ^\[main\.assertion\.\d+\] .* assertion data\[5\] == 0: FAILURE$ ^\[main\.assertion\.\d+\] .* assertion data\[5\] == 1: FAILURE$ ^VERIFICATION FAILED$ diff --git a/regression/contracts/invar_havoc_static_array_const_idx/test.desc b/regression/contracts/invar_havoc_static_array_const_idx/test.desc index 45adf3e6982..0dfc45afdcf 100644 --- a/regression/contracts/invar_havoc_static_array_const_idx/test.desc +++ b/regression/contracts/invar_havoc_static_array_const_idx/test.desc @@ -6,7 +6,7 @@ main.c ^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$ ^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$ ^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ -^\[main.assigns.\d+\] .* Check that data\[\(signed long (long )?int\)1\] is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that data\[(\(signed long (long )?int\))?1\] is assignable: SUCCESS$ ^\[main\.assertion\.\d+\] .* assertion data\[1\] == 0 \|\| data\[1\] == 1: FAILURE$ ^\[main\.assertion\.\d+\] .* assertion data\[4\] == 0: SUCCESS$ ^VERIFICATION FAILED$ diff --git a/regression/contracts/invar_havoc_static_multi-dim_array_all_const_idx/test.desc b/regression/contracts/invar_havoc_static_multi-dim_array_all_const_idx/test.desc index 052fe5af389..01204c9ab18 100644 --- a/regression/contracts/invar_havoc_static_multi-dim_array_all_const_idx/test.desc +++ b/regression/contracts/invar_havoc_static_multi-dim_array_all_const_idx/test.desc @@ -5,7 +5,7 @@ main.c ^SIGNAL=0$ ^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$ ^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$ -^\[main.assigns.\d+\] .* Check that data\[\(signed long (long )?int\)4\]\[\(signed long (long )?int\)5\]\[\(signed long (long )?int\)6\] is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that data\[(\(signed long (long )?int\))?4\]\[(\(signed long (long )?int\))?5\]\[(\(signed long (long )?int\))?6\] is assignable: SUCCESS$ ^\[main\.assertion\.\d+\] .* assertion data\[4\]\[5\]\[6\] == 0: FAILURE$ ^\[main\.assertion\.\d+\] .* assertion data\[1\]\[2\]\[3\] == 0: SUCCESS$ ^VERIFICATION FAILED$ diff --git a/regression/contracts/invar_havoc_static_multi-dim_array_partial_const_idx/test.desc b/regression/contracts/invar_havoc_static_multi-dim_array_partial_const_idx/test.desc index 6ec32feb580..cda08ce2639 100644 --- a/regression/contracts/invar_havoc_static_multi-dim_array_partial_const_idx/test.desc +++ b/regression/contracts/invar_havoc_static_multi-dim_array_partial_const_idx/test.desc @@ -6,7 +6,7 @@ main.c ^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$ ^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$ ^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ -^\[main.assigns.\d+\] .* Check that data\[\(signed long (long )?int\)4\]\[\(signed long (long )?int\)i\]\[\(signed long (long )?int\)6\] is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that data\[(\(signed long (long )?int\))?4\]\[(\(signed (long (long )?)?int\))?i\]\[(\(signed long (long )?int\))?6\] is assignable: SUCCESS$ ^\[main\.assertion\.\d+\] .* assertion data\[1\]\[2\]\[3\] == 0: FAILURE$ ^\[main\.assertion\.\d+\] .* assertion data\[4\]\[5\]\[6\] == 0: FAILURE$ ^VERIFICATION FAILED$ diff --git a/regression/contracts/loop_assigns-slice-assignable-scalar/test.desc b/regression/contracts/loop_assigns-slice-assignable-scalar/test.desc index 09f56c97fad..3ab6f3105b4 100644 --- a/regression/contracts/loop_assigns-slice-assignable-scalar/test.desc +++ b/regression/contracts/loop_assigns-slice-assignable-scalar/test.desc @@ -5,10 +5,10 @@ main.c ^SIGNAL=0$ ^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$ ^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ -^\[main.assigns.\d+\] .* Check that b->data\[\(.*\)0\] is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that b->data\[(\(.*\))?0\] is assignable: SUCCESS$ ^\[main.assigns.\d+\] .* Check that b->data\[\(.*\)i\] is assignable: FAILURE$ ^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$ -^\[main.assigns.\d+\] .* Check that __CPROVER_assignable\(\(.*\)&b->data\[\(.*\)0\], 1ul?l?, FALSE\) is valid: SUCCESS$ +^\[main.assigns.\d+\] .* Check that __CPROVER_assignable\(\(.*\)&b->data\[(\(.*\))?0\], 1ul?l?, FALSE\) is valid: SUCCESS$ ^\[main.assertion.\d+\] .* assertion b->data\[0\] == 0: FAILURE$ ^\[main.assertion.\d+\] .* assertion b->data\[1\] == 0: SUCCESS$ ^\[main.assertion.\d+\] .* assertion b->data\[2\] == 0: SUCCESS$ diff --git a/regression/contracts/loop_assigns-slice-upto-fail/test.desc b/regression/contracts/loop_assigns-slice-upto-fail/test.desc index 7b9a85314ad..4300f9931ef 100644 --- a/regression/contracts/loop_assigns-slice-upto-fail/test.desc +++ b/regression/contracts/loop_assigns-slice-upto-fail/test.desc @@ -4,10 +4,10 @@ main.c ^\[main.\d+\] .* Check loop invariant before entry: SUCCESS$ ^\[main.\d+\] .* Check that loop invariant is preserved: SUCCESS$ ^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ -^\[main.assigns.\d+\] .* Check that b->data\[\(.*\)0\] is assignable: SUCCESS$ -^\[main.assigns.\d+\] .* Check that b->data\[\(.*\)1\] is assignable: SUCCESS$ -^\[main.assigns.\d+\] .* Check that b->data\[\(.*\)2\] is assignable: SUCCESS$ -^\[main.assigns.\d+\] .* Check that b->data\[\(.*\)i\] is assignable: FAILURE$ +^\[main.assigns.\d+\] .* Check that b->data\[(\(.*\))?0\] is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that b->data\[(\(.*\))?1\] is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that b->data\[(\(.*\))?2\] is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that b->data\[(\(.*\))?i\] is assignable: FAILURE$ ^\[main.assertion.\d+\] .* assertion b->data\[0\] == 0: FAILURE$ ^\[main.assertion.\d+\] .* assertion b->data\[1\] == 0: FAILURE$ ^\[main.assertion.\d+\] .* assertion b->data\[2\] == 0: FAILURE$ diff --git a/regression/contracts/loop_contracts_binary_search/main.c b/regression/contracts/loop_contracts_binary_search/main.c index 18a3cd67ff3..deaf50081f5 100644 --- a/regression/contracts/loop_contracts_binary_search/main.c +++ b/regression/contracts/loop_contracts_binary_search/main.c @@ -32,7 +32,8 @@ int binary_search(int val, int *buf, int size) int main() { - int val, size; + int val; + char size; int *buf = size >= 0 ? malloc(size * sizeof(int)) : NULL; int idx = binary_search(val, buf, size); diff --git a/regression/contracts/quantifiers-forall-ensures-enforce/test.desc b/regression/contracts/quantifiers-forall-ensures-enforce/test.desc index ebd37152ecf..77d7c1e018a 100644 --- a/regression/contracts/quantifiers-forall-ensures-enforce/test.desc +++ b/regression/contracts/quantifiers-forall-ensures-enforce/test.desc @@ -4,11 +4,11 @@ main.c ^EXIT=0$ ^SIGNAL=0$ ^\[f1.postcondition.\d+\] line \d+ Check ensures clause: SUCCESS$ -^\[f1.assigns.\d+\] line \d+ Check that arr\[\(.*\)\d\] is assignable: SUCCESS$ +^\[f1.assigns.\d+\] line \d+ Check that arr\[(\(.*\))?\d\] is assignable: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- ^warning: ignoring -^\[f1.assigns.\d+\] line \d+ Check that arr\[\(.*\)\d\] is assignable: FAILURE$ +^\[f1.assigns.\d+\] line \d+ Check that arr\[(\(.*\))?\d\] is assignable: FAILURE$ -- The purpose of this test is to ensure that we can safely use __CPROVER_forall within positive contexts (enforced ENSURES clauses). diff --git a/regression/contracts/quantifiers-loop-01/test.desc b/regression/contracts/quantifiers-loop-01/test.desc index 2b61263b997..db0339d788d 100644 --- a/regression/contracts/quantifiers-loop-01/test.desc +++ b/regression/contracts/quantifiers-loop-01/test.desc @@ -6,7 +6,7 @@ main.c ^\[main\.\d+\] line .* Check loop invariant before entry: SUCCESS$ ^\[main\.\d+\] line .* Check that loop invariant is preserved: SUCCESS$ ^\[main.assigns.\d+\] line .* Check that i is assignable: SUCCESS$ -^\[main.assigns.\d+\] line .* Check that a\[\(signed long (long )?int\)i\] is assignable: SUCCESS$ +^\[main.assigns.\d+\] line .* Check that a\[(\(signed long (long )?int\))?i\] is assignable: SUCCESS$ ^\[main\.assertion\.\d+\] line .* assertion a\[10\] == 1: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- diff --git a/regression/contracts/quantifiers-loop-02/test.desc b/regression/contracts/quantifiers-loop-02/test.desc index 6d2b3c39772..3ae97f80f22 100644 --- a/regression/contracts/quantifiers-loop-02/test.desc +++ b/regression/contracts/quantifiers-loop-02/test.desc @@ -6,7 +6,7 @@ main.c ^\[main.\d+\] line .* Check loop invariant before entry: SUCCESS$ ^\[main.\d+\] line .* Check that loop invariant is preserved: SUCCESS$ ^\[main.assigns.\d+\] line .* Check that i is assignable: SUCCESS$ -^\[main.assigns.\d+\] line .* Check that a\[\(signed long (long )?int\)i\] is assignable: SUCCESS$ +^\[main.assigns.\d+\] line .* Check that a\[(\(signed long (long )?int\))?i\] is assignable: SUCCESS$ ^\[main.assertion.\d+\] line .* assertion .*: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- diff --git a/regression/contracts/quantifiers-loop-03/test.desc b/regression/contracts/quantifiers-loop-03/test.desc index faeedaec836..86140e129eb 100644 --- a/regression/contracts/quantifiers-loop-03/test.desc +++ b/regression/contracts/quantifiers-loop-03/test.desc @@ -6,7 +6,7 @@ main.c ^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$ ^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$ ^\[main.assigns.\d+\] .* Check that i is assignable: SUCCESS$ -^\[main.assigns.\d+\] .* Check that a\[\(signed long (long )?int\)i\] is assignable: SUCCESS$ +^\[main.assigns.\d+\] .* Check that a\[(\(signed long (long )?int\))?i\] is assignable: SUCCESS$ ^\[main\.assertion\.\d+\] line .* assertion .*: SUCCESS$ ^VERIFICATION SUCCESSFUL$ -- diff --git a/regression/cprover/arrays/array2.desc b/regression/cprover/arrays/array2.desc index c9d515beef2..5ca669c8151 100644 --- a/regression/cprover/arrays/array2.desc +++ b/regression/cprover/arrays/array2.desc @@ -4,8 +4,8 @@ array2.c ^EXIT=10$ ^SIGNAL=0$ ^\(\d+\) ∀ ς : state \. \(S13\(ς\) ∧ ς\(❝main::1::i❞\) = ς\(❝main::1::j❞\)\) ⇒ S14\(ς\)$ -^\(\d+\) ∀ ς : state \. S14\(ς\) ⇒ \(ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::i❞\), signedbv\[64\]\)\)\) = ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::j❞\), signedbv\[64\]\)\)\)\)$ -^\(\d+\) ∀ ς : state \. S15\(ς\) ⇒ \(ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::i❞\), signedbv\[64\]\)\)\) = ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::k❞\), signedbv\[64\]\)\)\)\)$ +^\(\d+\) ∀ ς : state \. S14\(ς\) ⇒ \(ς\(element_address\(❝main::1::array❞, (ς\(❝main::1::i❞\)|cast\(ς\(❝main::1::i❞\), signedbv\[64\]\))\)\) = ς\(element_address\(❝main::1::array❞, (ς\(❝main::1::j❞\)|cast\(ς\(❝main::1::j❞\), signedbv\[64\]\))\)\)\)$ +^\(\d+\) ∀ ς : state \. S15\(ς\) ⇒ \(ς\(element_address\(❝main::1::array❞, (ς\(❝main::1::i❞\)|cast\(ς\(❝main::1::i❞\), signedbv\[64\]\))\)\) = ς\(element_address\(❝main::1::array❞, (ς\(❝main::1::k❞\)|cast\(ς\(❝main::1::k❞\), signedbv\[64\]\))\)\)\)$ ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$ ^\[main\.assertion\.2\] line \d+ property 2: REFUTED$ -- diff --git a/regression/cprover/loops/given_invariant8.c b/regression/cprover/loops/given_invariant8.c index 2d09d76ddcd..fbdee28134f 100644 --- a/regression/cprover/loops/given_invariant8.c +++ b/regression/cprover/loops/given_invariant8.c @@ -1,6 +1,6 @@ int main() { - int n; + char n; __CPROVER_assume(n >= 0); int array[n]; diff --git a/regression/cprover/loops/given_invariant9.c b/regression/cprover/loops/given_invariant9.c index 32b407a2b97..1b386ddc60d 100644 --- a/regression/cprover/loops/given_invariant9.c +++ b/regression/cprover/loops/given_invariant9.c @@ -2,7 +2,7 @@ void *malloc(__CPROVER_size_t); int main() { - int n; + char n; __CPROVER_assume(n >= 0); int *array = malloc(sizeof(int) * n); diff --git a/regression/cprover/pointers/malloc1.desc b/regression/cprover/pointers/malloc1.desc index b592ec6376d..3b957873d6c 100644 --- a/regression/cprover/pointers/malloc1.desc +++ b/regression/cprover/pointers/malloc1.desc @@ -3,6 +3,6 @@ malloc1.c --text --solve --inline ^EXIT=0$ ^SIGNAL=0$ -^\(\d+\) ∀ ς : state \. S11\(ς\) ⇒ S12\(ς\[❝main::\$tmp::return_value_malloc❞:=allocate\(ς, 4 \* cast\(10, unsignedbv\[64\]\)\)\]\)$ +^\(\d+\) ∀ ς : state \. S11\(ς\) ⇒ S12\(ς\[❝main::\$tmp::return_value_malloc❞:=allocate\(ς, 4 \* cast\(10, unsignedbv\[\d+\]\)\)\]\)$ ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$ -- diff --git a/regression/goto-analyzer/constant_propagation_01/test-vsd.desc b/regression/goto-analyzer/constant_propagation_01/test-vsd.desc index 741965ab2a5..857663aae54 100644 --- a/regression/goto-analyzer/constant_propagation_01/test-vsd.desc +++ b/regression/goto-analyzer/constant_propagation_01/test-vsd.desc @@ -3,7 +3,7 @@ main.c --variable-sensitivity --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 2, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 9, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 1, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 10, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_01/test.desc b/regression/goto-analyzer/constant_propagation_01/test.desc index e0147b4ce18..0af17335395 100644 --- a/regression/goto-analyzer/constant_propagation_01/test.desc +++ b/regression/goto-analyzer/constant_propagation_01/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 2, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 9, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 1, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 10, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_02/test-vsd.desc b/regression/goto-analyzer/constant_propagation_02/test-vsd.desc index db447649547..741965ab2a5 100644 --- a/regression/goto-analyzer/constant_propagation_02/test-vsd.desc +++ b/regression/goto-analyzer/constant_propagation_02/test-vsd.desc @@ -3,7 +3,7 @@ main.c --variable-sensitivity --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 3, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 8, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 2, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 9, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_02/test.desc b/regression/goto-analyzer/constant_propagation_02/test.desc index f8465991235..e0147b4ce18 100644 --- a/regression/goto-analyzer/constant_propagation_02/test.desc +++ b/regression/goto-analyzer/constant_propagation_02/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 3, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 8, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 2, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 9, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_03/test-vsd.desc b/regression/goto-analyzer/constant_propagation_03/test-vsd.desc index db447649547..741965ab2a5 100644 --- a/regression/goto-analyzer/constant_propagation_03/test-vsd.desc +++ b/regression/goto-analyzer/constant_propagation_03/test-vsd.desc @@ -3,7 +3,7 @@ main.c --variable-sensitivity --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 3, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 8, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 2, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 9, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_03/test.desc b/regression/goto-analyzer/constant_propagation_03/test.desc index f8465991235..e0147b4ce18 100644 --- a/regression/goto-analyzer/constant_propagation_03/test.desc +++ b/regression/goto-analyzer/constant_propagation_03/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 3, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 8, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 2, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 9, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_04/test-vsd.desc b/regression/goto-analyzer/constant_propagation_04/test-vsd.desc index db447649547..741965ab2a5 100644 --- a/regression/goto-analyzer/constant_propagation_04/test-vsd.desc +++ b/regression/goto-analyzer/constant_propagation_04/test-vsd.desc @@ -3,7 +3,7 @@ main.c --variable-sensitivity --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 3, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 8, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 2, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 9, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_04/test.desc b/regression/goto-analyzer/constant_propagation_04/test.desc index f8465991235..e0147b4ce18 100644 --- a/regression/goto-analyzer/constant_propagation_04/test.desc +++ b/regression/goto-analyzer/constant_propagation_04/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 3, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 8, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 2, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 0, assigns: 9, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_07/test-vsd.desc b/regression/goto-analyzer/constant_propagation_07/test-vsd.desc index 14364a509af..e7642b72f93 100644 --- a/regression/goto-analyzer/constant_propagation_07/test-vsd.desc +++ b/regression/goto-analyzer/constant_propagation_07/test-vsd.desc @@ -3,7 +3,7 @@ main.c --variable-sensitivity --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 3, assigns: 4, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 10, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 3, assigns: 3, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 11, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_07/test.desc b/regression/goto-analyzer/constant_propagation_07/test.desc index 3b836b8dad2..c9d6348e832 100644 --- a/regression/goto-analyzer/constant_propagation_07/test.desc +++ b/regression/goto-analyzer/constant_propagation_07/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 3, assigns: 4, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 10, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 3, assigns: 3, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 11, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_08/test-vsd.desc b/regression/goto-analyzer/constant_propagation_08/test-vsd.desc index b478301d9ee..922c1e85ddc 100644 --- a/regression/goto-analyzer/constant_propagation_08/test-vsd.desc +++ b/regression/goto-analyzer/constant_propagation_08/test-vsd.desc @@ -3,7 +3,7 @@ main.c --variable-sensitivity --vsd-arrays every-element --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 3, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 2, assigns: 7, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: [12], function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 2, assigns: [89], function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_08/test.desc b/regression/goto-analyzer/constant_propagation_08/test.desc index 52d013d15f5..4cee20fb9dc 100644 --- a/regression/goto-analyzer/constant_propagation_08/test.desc +++ b/regression/goto-analyzer/constant_propagation_08/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 2, assigns: 5, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 4, assigns: 13, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 2, assigns: 4, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 4, assigns: 14, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_11/test-vsd.desc b/regression/goto-analyzer/constant_propagation_11/test-vsd.desc index 90e1b48f887..79e36862d34 100644 --- a/regression/goto-analyzer/constant_propagation_11/test-vsd.desc +++ b/regression/goto-analyzer/constant_propagation_11/test-vsd.desc @@ -3,7 +3,7 @@ main.c --variable-sensitivity --vsd-arrays every-element --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 3, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 6, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: [12], function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 1, assigns: [78], function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_11/test.desc b/regression/goto-analyzer/constant_propagation_11/test.desc index bba19b94b66..9ddd84040d5 100644 --- a/regression/goto-analyzer/constant_propagation_11/test.desc +++ b/regression/goto-analyzer/constant_propagation_11/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 3, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 6, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: [12], function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 1, assigns: [78], function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_12/test-vsd.desc b/regression/goto-analyzer/constant_propagation_12/test-vsd.desc index e8b6c2d034f..a8ee1e377f3 100644 --- a/regression/goto-analyzer/constant_propagation_12/test-vsd.desc +++ b/regression/goto-analyzer/constant_propagation_12/test-vsd.desc @@ -3,7 +3,7 @@ main.c --variable-sensitivity --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 2, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 7, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 1, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 8, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/constant_propagation_12/test.desc b/regression/goto-analyzer/constant_propagation_12/test.desc index 614698c7277..9493668327f 100644 --- a/regression/goto-analyzer/constant_propagation_12/test.desc +++ b/regression/goto-analyzer/constant_propagation_12/test.desc @@ -3,7 +3,7 @@ main.c --constants --simplify out.gb ^EXIT=0$ ^SIGNAL=0$ -^Simplified: assert: 1, assume: 0, goto: 1, assigns: 2, function calls: 0$ -^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 7, function calls: 2$ +^Simplified: assert: 1, assume: 0, goto: 1, assigns: 1, function calls: 0$ +^Unmodified: assert: 0, assume: 0, goto: 1, assigns: 8, function calls: 2$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/variable-sensitivity-dependence-graph-toyota/test.desc b/regression/goto-analyzer/variable-sensitivity-dependence-graph-toyota/test.desc index cd3a57851d6..1662978999d 100644 --- a/regression/goto-analyzer/variable-sensitivity-dependence-graph-toyota/test.desc +++ b/regression/goto-analyzer/variable-sensitivity-dependence-graph-toyota/test.desc @@ -8,19 +8,19 @@ file1.c file2.c --dependence-graph-vs --vsd-structs every-field --vsd-arrays eve ^Data dependencies: 1 \[st.a\], 48 \[st.a\]$ ^Data dependencies: 4 \[st.b\], 48 \[st.b\]$ ^Data dependencies: 1 \[st.a\], 4 \[st.b\], 48 \[st.a, st.b\]$ -^Data dependencies: 42 \[ar\[\([^)]*\)0\]\]$ -^Data dependencies: 42 \[ar\[\([^)]*\)1\]\]$ -^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 42 \[ar\[\([^)]*\)0\]\]$ -^Data dependencies: 13 \[ar\[\([^)]*\)1\]\], 42 \[ar\[\([^)]*\)1\]\]$ -^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 13 \[ar\[\([^)]*\)1\]\], 42 \[ar\[\([^)]*\)0\], ar\[\([^)]*\)1\]\]$ -^Data dependencies: 19 \[arr\[\([^)]*\)1\]\]$ -^Data dependencies: 18 \[arr\[\([^)]*\)0\]\]$ -^Data dependencies: 20 \[arr\[\([^)]*\)2\]\], 22 \[arr\[\([^)]*\)2\]\]$ +^Data dependencies: 42 \[ar\[(\([^)]*\))?0\]\]$ +^Data dependencies: 42 \[ar\[(\([^)]*\))?1\]\]$ +^Data dependencies: 10 \[ar\[(\([^)]*\))?0\]\], 42 \[ar\[(\([^)]*\))?0\]\]$ +^Data dependencies: 13 \[ar\[(\([^)]*\))?1\]\], 42 \[ar\[(\([^)]*\))?1\]\]$ +^Data dependencies: 10 \[ar\[(\([^)]*\))?0\]\], 13 \[ar\[(\([^)]*\))?1\]\], 42 \[ar\[(\([^)]*\))?0\], ar\[(\([^)]*\))?1\]\]$ +^Data dependencies: 19 \[arr\[(\([^)]*\))?1\]\]$ +^Data dependencies: 18 \[arr\[(\([^)]*\))?0\]\]$ +^Data dependencies: 20 \[arr\[(\([^)]*\))?2\]\], 22 \[arr\[(\([^)]*\))?2\]\]$ ^Data dependencies: 1 \[st.a\], 48 \[st.a\], 52 \[st.a\]$ ^Data dependencies: 4 \[st.b\], 48 \[st.b\], 55 \[st.b\]$ ^Data dependencies: 1 \[st.a\], 4 \[st.b\], 48 \[st.a, st.b\], 52 \[st.a\], 55 \[st.b\]$ -^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 42 \[ar\[\([^)]*\)0\]\], 63 \[ar\[\([^)]*\)0\]\]$ -^Data dependencies: 13 \[ar\[\([^)]*\)1\]\], 42 \[ar\[\([^)]*\)1\]\], 66 \[ar\[\([^)]*\)1\]\]$ -^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 13 \[ar\[\([^)]*\)1\]\], 42 \[ar\[\([^)]*\)0\], ar\[\([^)]*\)1\]\], 63 \[ar\[\([^)]*\)0\]\], 66 \[ar\[\([^)]*\)1\]\]$ +^Data dependencies: 10 \[ar\[(\([^)]*\))?0\]\], 42 \[ar\[(\([^)]*\))?0\]\], 63 \[ar\[(\([^)]*\))?0\]\]$ +^Data dependencies: 13 \[ar\[(\([^)]*\))?1\]\], 42 \[ar\[(\([^)]*\))?1\]\], 66 \[ar\[(\([^)]*\))?1\]\]$ +^Data dependencies: 10 \[ar\[(\([^)]*\))?0\]\], 13 \[ar\[(\([^)]*\))?1\]\], 42 \[ar\[(\([^)]*\))?0\], ar\[(\([^)]*\))?1\]\], 63 \[ar\[(\([^)]*\))?0\]\], 66 \[ar\[(\([^)]*\))?1\]\]$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/variable-sensitivity-dependence-graph/test.desc b/regression/goto-analyzer/variable-sensitivity-dependence-graph/test.desc index 8abe0ffdcec..ff2a997bff0 100644 --- a/regression/goto-analyzer/variable-sensitivity-dependence-graph/test.desc +++ b/regression/goto-analyzer/variable-sensitivity-dependence-graph/test.desc @@ -8,20 +8,20 @@ file1.c file2.c --dependence-graph-vs --vsd-structs every-field --vsd-arrays eve ^Data dependencies: 1 \[st.a\], 48 \[st.a\]$ ^Data dependencies: 4 \[st.b\], 48 \[st.b\]$ ^Data dependencies: 1 \[st.a\], 4 \[st.b\], 48 \[st.a, st.b\]$ -^Data dependencies: 42 \[ar\[\([^)]*\)0\]\]$ +^Data dependencies: 42 \[ar\[(\([^)]*\))?0\]\]$ ^Data dependencies: 6 \[out1\]$ -^Data dependencies: 42 \[ar\[\([^)]*\)1\]\]$ -^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 42 \[ar\[\([^)]*\)0\]\]$ -^Data dependencies: 13 \[ar\[\([^)]*\)1\]\], 42 \[ar\[\([^)]*\)1\]\]$ -^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 13 \[ar\[\([^)]*\)1\]\], 42 \[ar\[\([^)]*\)0\], ar\[\([^)]*\)1\]\]$ -^Data dependencies: 19 \[arr\[\([^)]*\)1\]\]$ -^Data dependencies: 18 \[arr\[\([^)]*\)0\]\]$ -^Data dependencies: 20 \[arr\[\([^)]*\)2\]\], 22 \[arr\[\([^)]*\)2\]\]$ +^Data dependencies: 42 \[ar\[(\([^)]*\))?1\]\]$ +^Data dependencies: 10 \[ar\[(\([^)]*\))?0\]\], 42 \[ar\[(\([^)]*\))?0\]\]$ +^Data dependencies: 13 \[ar\[(\([^)]*\))?1\]\], 42 \[ar\[(\([^)]*\))?1\]\]$ +^Data dependencies: 10 \[ar\[(\([^)]*\))?0\]\], 13 \[ar\[(\([^)]*\))?1\]\], 42 \[ar\[(\([^)]*\))?0\], ar\[(\([^)]*\))?1\]\]$ +^Data dependencies: 19 \[arr\[(\([^)]*\))?1\]\]$ +^Data dependencies: 18 \[arr\[(\([^)]*\))?0\]\]$ +^Data dependencies: 20 \[arr\[(\([^)]*\))?2\]\], 22 \[arr\[(\([^)]*\))?2\]\]$ ^Data dependencies: 1 \[st.a\], 48 \[st.a\], 52 \[st.a\]$ ^Data dependencies: 4 \[st.b\], 48 \[st.b\], 55 \[st.b\]$ ^Data dependencies: 1 \[st.a\], 4 \[st.b\], 48 \[st.a, st.b\], 52 \[st.a\], 55 \[st.b\]$ -^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 42 \[ar\[\([^)]*\)0\]\], 63 \[ar\[\([^)]*\)0\]\]$ -^Data dependencies: 13 \[ar\[\([^)]*\)1\]\], 42 \[ar\[\([^)]*\)1\]\], 66 \[ar\[\([^)]*\)1\]\]$ -^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 13 \[ar\[\([^)]*\)1\]\], 42 \[ar\[\([^)]*\)0\], ar\[\([^)]*\)1\]\], 63 \[ar\[\([^)]*\)0\]\], 66 \[ar\[\([^)]*\)1\]\]$ +^Data dependencies: 10 \[ar\[(\([^)]*\))?0\]\], 42 \[ar\[(\([^)]*\))?0\]\], 63 \[ar\[(\([^)]*\))?0\]\]$ +^Data dependencies: 13 \[ar\[(\([^)]*\))?1\]\], 42 \[ar\[(\([^)]*\))?1\]\], 66 \[ar\[(\([^)]*\))?1\]\]$ +^Data dependencies: 10 \[ar\[(\([^)]*\))?0\]\], 13 \[ar\[(\([^)]*\))?1\]\], 42 \[ar\[(\([^)]*\))?0\], ar\[(\([^)]*\))?1\]\], 63 \[ar\[(\([^)]*\))?0\]\], 66 \[ar\[(\([^)]*\))?1\]\]$ -- ^warning: ignoring diff --git a/regression/goto-analyzer/variable-sensitivity-dependence-graph17/test.desc b/regression/goto-analyzer/variable-sensitivity-dependence-graph17/test.desc index 8bae062cd04..f4d952a3a3f 100644 --- a/regression/goto-analyzer/variable-sensitivity-dependence-graph17/test.desc +++ b/regression/goto-analyzer/variable-sensitivity-dependence-graph17/test.desc @@ -4,5 +4,5 @@ main.c activate-multi-line-match ^EXIT=0$ ^SIGNAL=0$ -\*\*\*\* 9 file .*main\.c line 22 function main\nControl dependencies: 24 \[UNCONDITIONAL\]\nData dependencies: 1 \[g_a\[\([^)]*\)i\]\], 2 \[g_a\[\([^)]*\)i\]\], 3 \[g_a\[\([^)]*\)i\]\], 7 \[g_a\[\([^)]*\)i\]\] +\*\*\*\* 9 file .*main\.c line 22 function main\nControl dependencies: 24 \[UNCONDITIONAL\]\nData dependencies: 1 \[g_a\[(\([^)]*\))?i\]\], 2 \[g_a\[(\([^)]*\))?i\]\], 3 \[g_a\[(\([^)]*\))?i\]\], 7 \[g_a\[(\([^)]*\))?i\]\] -- diff --git a/regression/goto-harness/chain.sh b/regression/goto-harness/chain.sh index cb04d75bdd3..c9f796abfc2 100755 --- a/regression/goto-harness/chain.sh +++ b/regression/goto-harness/chain.sh @@ -24,6 +24,23 @@ fi args=${*:1:$#-1} +cleanup() +{ + rm -f "$needs_cleaning" +} + +needs_cleaning="" +trap cleanup EXIT + +json_file=`echo $args | grep '\.json' | sed 's/\.json.*/.json/' | sed 's/.* //'` +if [[ "x$json_file" != "x" ]]; then + bit_width=`$goto_harness -h | grep -- -bit | sed 's/-bit.*//' | sed 's/.* //'` + if [[ "$bit_width" != "64" ]]; then + needs_cleaning="$json_file.$bit_width" + sed "s/\"id\": \"64\"/\"id\": \"$bit_width\"/" "$json_file" > "$json_file.$bit_width" + args=${args/$json_file/$json_file.$bit_width} + fi +fi if [[ "${is_windows}" == "true" ]]; then $goto_cc "$input_c_file" "/Fe$input_goto_binary" diff --git a/regression/goto-harness/pointer-to-array-function-parameters-max-size/test.desc b/regression/goto-harness/pointer-to-array-function-parameters-max-size/test.desc index a690f08c757..0b8dde7ed64 100644 --- a/regression/goto-harness/pointer-to-array-function-parameters-max-size/test.desc +++ b/regression/goto-harness/pointer-to-array-function-parameters-max-size/test.desc @@ -2,12 +2,12 @@ CORE test.c --harness-type call-function --function test --max-array-size 10 --associated-array-size arr:sz \[test.assertion.1\] line \d+ assertion sz < 10: FAILURE -\[test.pointer_dereference.\d+\] line \d+ dereference failure: pointer NULL in arr\[\(signed( long)* int\)i\]: SUCCESS -\[test.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in arr\[\(signed( long)* int\)i\]: SUCCESS -\[test.pointer_dereference.\d+\] line \d+ dereference failure: deallocated dynamic object in arr\[\(signed( long)* int\)i\]: SUCCESS -\[test.pointer_dereference.\d+\] line \d+ dereference failure: dead object in arr\[\(signed( long)* int\)i\]: SUCCESS -\[test.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[\(signed( long)* int\)i\]: SUCCESS -\[test.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[\(signed( long)* int\)i\]: SUCCESS +\[test.pointer_dereference.\d+\] line \d+ dereference failure: pointer NULL in arr\[(\(signed( long)* int\))?i\]: SUCCESS +\[test.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in arr\[(\(signed( long)* int\))?i\]: SUCCESS +\[test.pointer_dereference.\d+\] line \d+ dereference failure: deallocated dynamic object in arr\[(\(signed( long)* int\))?i\]: SUCCESS +\[test.pointer_dereference.\d+\] line \d+ dereference failure: dead object in arr\[(\(signed( long)* int\))?i\]: SUCCESS +\[test.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[(\(signed( long)* int\))?i\]: SUCCESS +\[test.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[(\(signed( long)* int\))?i\]: SUCCESS ^EXIT=10$ ^SIGNAL=0$ -- diff --git a/regression/goto-harness/pointer-to-array-function-parameters-multi-arg-wrong/test.desc b/regression/goto-harness/pointer-to-array-function-parameters-multi-arg-wrong/test.desc index d37096e99bc..687cc754814 100644 --- a/regression/goto-harness/pointer-to-array-function-parameters-multi-arg-wrong/test.desc +++ b/regression/goto-harness/pointer-to-array-function-parameters-multi-arg-wrong/test.desc @@ -3,6 +3,6 @@ test.c --harness-type call-function --function is_prefix_of --treat-pointer-as-array string --treat-pointer-as-array prefix --associated-array-size string:string_size --associated-array-size prefix:prefix_size --max-array-size 5 ^EXIT=10$ ^SIGNAL=0$ -\[is_prefix_of.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in prefix\[\(signed( long)* int\)ix\]: FAILURE +\[is_prefix_of.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in prefix\[(\(signed( long)* int\))?ix\]: FAILURE VERIFICATION FAILED -- diff --git a/regression/goto-harness/pointer-to-array-function-parameters-with-size/test.desc b/regression/goto-harness/pointer-to-array-function-parameters-with-size/test.desc index 2d09e75635c..0bce259ad7b 100644 --- a/regression/goto-harness/pointer-to-array-function-parameters-with-size/test.desc +++ b/regression/goto-harness/pointer-to-array-function-parameters-with-size/test.desc @@ -3,9 +3,9 @@ test.c --harness-type call-function --function test --treat-pointer-as-array arr --associated-array-size arr:sz ^EXIT=0$ ^SIGNAL=0$ -\[test.pointer_dereference.1\] line \d+ dereference failure: pointer NULL in arr\[\(signed( long)* int\)i\]: SUCCESS -\[test.pointer_dereference.2\] line \d+ dereference failure: pointer invalid in arr\[\(signed( long)* int\)i\]: SUCCESS -\[test.pointer_dereference.3\] line \d+ dereference failure: deallocated dynamic object in arr\[\(signed( long)* int\)i\]: SUCCESS -\[test.pointer_dereference.4\] line \d+ dereference failure: dead object in arr\[\(signed( long)* int\)i\]: SUCCESS -\[test.pointer_dereference.5\] line \d+ dereference failure: pointer outside object bounds in arr\[\(signed( long)* int\)i\]: SUCCESS +\[test.pointer_dereference.1\] line \d+ dereference failure: pointer NULL in arr\[(\(signed( long)* int\))?i\]: SUCCESS +\[test.pointer_dereference.2\] line \d+ dereference failure: pointer invalid in arr\[(\(signed( long)* int\))?i\]: SUCCESS +\[test.pointer_dereference.3\] line \d+ dereference failure: deallocated dynamic object in arr\[(\(signed( long)* int\))?i\]: SUCCESS +\[test.pointer_dereference.4\] line \d+ dereference failure: dead object in arr\[(\(signed( long)* int\))?i\]: SUCCESS +\[test.pointer_dereference.5\] line \d+ dereference failure: pointer outside object bounds in arr\[(\(signed( long)* int\))?i\]: SUCCESS -- diff --git a/regression/goto-harness/pointer-to-array-function-parameters/test.desc b/regression/goto-harness/pointer-to-array-function-parameters/test.desc index f010f238e1b..337b161660a 100644 --- a/regression/goto-harness/pointer-to-array-function-parameters/test.desc +++ b/regression/goto-harness/pointer-to-array-function-parameters/test.desc @@ -1,8 +1,8 @@ CORE test.c --harness-type call-function --function test --treat-pointer-as-array arr -\[test.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[\(signed( long)* int\)0\]: SUCCESS -\[test.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[\(signed( long)* int\)10\]: FAILURE +\[test.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[(\(signed( long)* int\))?0\]: SUCCESS +\[test.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in arr\[(\(signed( long)* int\))?10\]: FAILURE ^EXIT=10$ ^SIGNAL=0$ -- diff --git a/regression/goto-inspect/show-goto-functions/positive.desc b/regression/goto-inspect/show-goto-functions/positive.desc index 7d2149d8274..f2702137cc7 100644 --- a/regression/goto-inspect/show-goto-functions/positive.desc +++ b/regression/goto-inspect/show-goto-functions/positive.desc @@ -4,9 +4,9 @@ main.c ^EXIT=0$ ^SIGNAL=0$ main -DECL main::1::arr : signedbv\[32\]\[5\] +DECL main::1::arr : signedbv\[\d+\]\[5\] ASSIGN main::1::arr := \{ 0, 1, 2, 3, 4 \} -ASSERT main::1::arr\[cast\(0, signedbv\[64\]\)\] ≠ 0 // Expected failure: 0 == 0 +ASSERT main::1::arr\[(0|cast\(0, signedbv\[\d+\]\))\] ≠ 0 // Expected failure: 0 == 0 DEAD main::1::arr SET RETURN VALUE side_effect statement="nondet" is_nondet_nullable="1" END_FUNCTION diff --git a/regression/goto-instrument/enable-pragmas/test.desc b/regression/goto-instrument/enable-pragmas/test.desc index 2ef5016ada8..8d3e3154585 100644 --- a/regression/goto-instrument/enable-pragmas/test.desc +++ b/regression/goto-instrument/enable-pragmas/test.desc @@ -1,11 +1,11 @@ CORE main.c -^\[main.array_bounds.\d+\] line \d+ array 'a' upper bound in a\[\(signed .* int\)2\]: FAILURE +^\[main.array_bounds.\d+\] line \d+ array 'a' upper bound in a\[(\(signed .* int\))?2\]: FAILURE ^VERIFICATION FAILED ^EXIT=10$ ^SIGNAL=0$ -- -- Checks that enable pragmas do not cause invariant failures when running goto-instrument -and cbmc in sequence. \ No newline at end of file +and cbmc in sequence. diff --git a/regression/memory-analyzer/chain.sh b/regression/memory-analyzer/chain.sh index ced497e139e..06631d756f5 100755 --- a/regression/memory-analyzer/chain.sh +++ b/regression/memory-analyzer/chain.sh @@ -12,5 +12,10 @@ args=$(echo $cmd | cut -d ' ' -f 2-) name=${name%.gb} opts=${*:3:$#-3} -$goto_gcc -g -std=c11 -o "${name}.gb" "${name}.c" +bit_width=`$memory_analyzer -h | grep -- -bit | sed 's/-bit.*//' | sed 's/.* //'` +if [[ "$bit_width" != "64" ]] && [[ $(uname -m) = "x86_64" ]]; then + $goto_gcc -g -m32 -std=c11 -o "${name}.gb" "${name}.c" +else + $goto_gcc -g -std=c11 -o "${name}.gb" "${name}.c" +fi $memory_analyzer $opts "${name}.gb" $args diff --git a/src/analyses/variable-sensitivity/abstract_pointer_object.cpp b/src/analyses/variable-sensitivity/abstract_pointer_object.cpp index 43b20ccf7d5..e5852b3b30c 100644 --- a/src/analyses/variable-sensitivity/abstract_pointer_object.cpp +++ b/src/analyses/variable-sensitivity/abstract_pointer_object.cpp @@ -99,7 +99,7 @@ abstract_object_pointert abstract_pointer_objectt::eval_ptr_diff( const namespacet &ns) const { if(is_top() || operands[1]->is_top()) - return environment.eval(nil_exprt(), ns); + return environment.abstract_object_factory(expr.type(), ns, true, false); return ptr_diff(expr, operands, environment, ns); } diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp index 294073fa93a..749353af3ce 100644 --- a/src/ansi-c/ansi_c_internal_additions.cpp +++ b/src/ansi-c/ansi_c_internal_additions.cpp @@ -183,8 +183,15 @@ void ansi_c_internal_additions(std::string &code) CPROVER_PREFIX "size_t " CPROVER_PREFIX "max_malloc_size="+ integer2string(max_malloc_size(config.ansi_c.pointer_width, config - .bv_encoding.object_bits))+";\n" + .bv_encoding.object_bits)); + if(config.ansi_c.pointer_width==config.ansi_c.long_int_width) + code += "UL;\n"; + else if(config.ansi_c.pointer_width==config.ansi_c.long_long_int_width) + code += "ULL;\n"; + else + code += "U;\n"; + code+= // this is ANSI-C "extern " CPROVER_PREFIX "thread_local const char __func__[" CPROVER_PREFIX "constant_infinity_uint];\n" diff --git a/src/ansi-c/library/cprover_contracts.c b/src/ansi-c/library/cprover_contracts.c index 602ce3b89c4..37c5e476093 100644 --- a/src/ansi-c/library/cprover_contracts.c +++ b/src/ansi-c/library/cprover_contracts.c @@ -13,7 +13,11 @@ extern const void *__CPROVER_deallocated; const void *__CPROVER_new_object = 0; extern const void *__CPROVER_memory_leak; __CPROVER_bool __CPROVER_malloc_is_new_array = 0; +#if defined(_WIN32) && defined(_M_X64) int __builtin_clzll(unsigned long long); +#else +int __builtin_clzl(unsigned long); +#endif __CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void); __CPROVER_size_t __VERIFIER_nondet_size(void); @@ -245,8 +249,13 @@ __CPROVER_HIDE:; // symex state from the number of object_bits/offset_bits // the number of object bits is determined by counting the number of leading // zeroes of the built-in constant __CPROVER_max_malloc_size; +#if defined(_WIN32) && defined(_M_X64) int object_bits = __builtin_clzll(__CPROVER_max_malloc_size); __CPROVER_size_t nof_objects = 1ULL << object_bits; +#else + int object_bits = __builtin_clzl(__CPROVER_max_malloc_size); + __CPROVER_size_t nof_objects = 1UL << object_bits; +#endif *set = (__CPROVER_contracts_obj_set_t){ .max_elems = nof_objects, .watermark = 0, diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp index e8dfd004329..7761d4d091f 100644 --- a/src/goto-programs/interpreter.cpp +++ b/src/goto-programs/interpreter.cpp @@ -10,11 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com /// Interpreter for GOTO Programs #include "interpreter.h" - -#include -#include -#include -#include +#include "interpreter_class.h" #include #include @@ -29,9 +25,14 @@ Author: Daniel Kroening, kroening@kroening.com #include #include "goto_model.h" -#include "interpreter_class.h" #include "json_goto_trace.h" +#include +#include +#include +#include +#include + const std::size_t interpretert::npos=std::numeric_limits::max(); void interpretert::operator()() @@ -958,13 +959,13 @@ bool interpretert::unbounded_size(const typet &type) } /// Retrieves the actual size of the provided structured type. Unbounded objects -/// get allocated 2^32 address space each (of a 2^64 sized space). +/// get allocated 2^(platform bit-width / 2 + 1) address space each. /// \param type: a structured type /// \return Size of the given type mp_integer interpretert::get_size(const typet &type) { if(unbounded_size(type)) - return mp_integer(2) << 32; + return mp_integer(2) << (sizeof(std::size_t) * CHAR_BIT / 2); if(type.id()==ID_struct) { diff --git a/src/memory-analyzer/analyze_symbol.cpp b/src/memory-analyzer/analyze_symbol.cpp index 6bff8a5472b..2c4ee0fae28 100644 --- a/src/memory-analyzer/analyze_symbol.cpp +++ b/src/memory-analyzer/analyze_symbol.cpp @@ -393,9 +393,9 @@ exprt gdb_value_extractort::get_non_char_pointer_value( // Check if pointer was dynamically allocated (via malloc). If so we will // replace the pointee with a static array filled with values stored at the - // expected positions. Since the allocated size is over-approximation we may - // end up querying pass the allocated bounds and building larger array with - // meaningless values. + // expected positions. Since the allocated size is an over-approximation we + // may end up querying past the allocated bounds and building a larger array + // with meaningless values. mp_integer allocated_size = get_malloc_size(c_converter.convert(expr)); // get the sizeof(target_type) and thus the number of elements const auto number_of_elements = allocated_size / get_type_size(target_type); @@ -406,7 +406,7 @@ exprt gdb_value_extractort::get_non_char_pointer_value( for(size_t i = 0; i < number_of_elements; i++) { const auto sub_expr_value = get_expr_value( - index_exprt{expr, from_integer(i, index_type())}, + dereference_exprt{plus_exprt{expr, from_integer(i, index_type())}}, *zero_expr, location); elements.push_back(sub_expr_value); diff --git a/src/memory-analyzer/gdb_api.cpp b/src/memory-analyzer/gdb_api.cpp index 65253ae3612..3ad72ffda24 100644 --- a/src/memory-analyzer/gdb_api.cpp +++ b/src/memory-analyzer/gdb_api.cpp @@ -287,7 +287,8 @@ void gdb_apit::run_gdb_from_core(const std::string &corefile) void gdb_apit::collect_malloc_calls() { - // this is what the registers look like at the function call entry: +#if defined(__x86_64__) + // this is what the registers look like at the function call entry for x86-64: // // reg. name hex. value dec. value // 0: rax 0xffffffff 4294967295 @@ -303,6 +304,17 @@ void gdb_apit::collect_malloc_calls() write_to_gdb("-data-list-register-values d 5"); auto record = get_most_recent_record("^done", true); auto allocated_size = safe_string2size_t(get_register_value(record)); +#elif defined(__i386__) + // x86 32-bit Linux calling conventions use the stack to pass arguments. The + // top of the stack is the return address, so look at the next element (+4 as + // the stack grows downwards). + write_to_gdb("-data-evaluate-expression \"*(unsigned long*)($esp + 4)\""); + auto record = get_most_recent_record("^done", true); + auto allocated_size = + safe_string2size_t(get_value_from_record(record, "value")); +#else +# error malloc calling conventions not know for current platform +#endif write_to_gdb("-exec-finish"); if(!most_recent_line_has_tag("*running")) @@ -324,7 +336,7 @@ void gdb_apit::collect_malloc_calls() record = get_most_recent_record("*stopped"); } - // now we can read the rax register to the the allocated memory address + // now we can read the eax/rax register to the allocated memory address write_to_gdb("-data-list-register-values x 0"); record = get_most_recent_record("^done", true); allocated_memory[get_register_value(record)] = allocated_size; diff --git a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp index 5f0a97ad98e..962f0ca9e66 100644 --- a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -165,6 +165,8 @@ extension_for_type(const typet &type) return smt_bit_vector_theoryt::zero_extend; if(can_cast_type(type)) return smt_bit_vector_theoryt::zero_extend; + if(can_cast_type(type)) + return smt_bit_vector_theoryt::zero_extend; UNREACHABLE; } diff --git a/src/util/config.cpp b/src/util/config.cpp index 7d08d5bedd2..a390435b264 100644 --- a/src/util/config.cpp +++ b/src/util/config.cpp @@ -1156,15 +1156,17 @@ bool configt::set(const cmdlinet &cmdline) else { // For other systems assume argc is no larger than the what would make argv - // consume all available memory space: - // 2^pointer_width / (pointer_width / char_width) is the maximum number of - // argv elements sysconf(ARG_MAX) is likely much lower than this, but we - // don't know that value for the verification target platform. + // the largest representable array (when using signed integers to represent + // array sizes): + // 2^(pointer_width - 1) / (pointer_width / char_width) is the maximum + // number of argv elements sysconf(ARG_MAX) is likely much lower than this, + // but we don't know that value for the verification target platform. const auto pointer_bits_2log = address_bits(ansi_c.pointer_width / ansi_c.char_width); - if(ansi_c.pointer_width - pointer_bits_2log <= ansi_c.int_width) + if(ansi_c.pointer_width - pointer_bits_2log - 1 <= ansi_c.int_width) { - ansi_c.max_argc = power(2, config.ansi_c.int_width - pointer_bits_2log); + ansi_c.max_argc = + power(2, config.ansi_c.int_width - pointer_bits_2log - 1); } // otherwise we leave argc unconstrained } diff --git a/unit/goto-programs/goto_program_validate.cpp b/unit/goto-programs/goto_program_validate.cpp index cba68ed1d56..64f77436953 100644 --- a/unit/goto-programs/goto_program_validate.cpp +++ b/unit/goto-programs/goto_program_validate.cpp @@ -10,12 +10,10 @@ /// \file /// Unit tests for goto program validation -#include - -#include - #include #include +#include +#include #include #include @@ -23,8 +21,16 @@ #include #include +#include +#include + SCENARIO("Validation of a goto program", "[core][goto-programs][validate]") { + // This test does require a proper architecture to be set so that C type + // widths are configured. + cmdlinet cmdline; + config.set(cmdline); + goto_modelt goto_model; // void f(){int x = 1;} @@ -54,8 +60,7 @@ SCENARIO("Validation of a goto program", "[core][goto-programs][validate]") goto_model.symbol_table.add(z); // pointer to fn call - symbolt fn_ptr{ - "fn_ptr", pointer_typet(code_typet{{}, empty_typet()}, 64), ID_C}; + symbolt fn_ptr{"fn_ptr", pointer_type(code_typet{{}, empty_typet()}), ID_C}; goto_model.symbol_table.add(fn_ptr); symbolt entry_point{ diff --git a/unit/interpreter/interpreter.cpp b/unit/interpreter/interpreter.cpp index f891fa6b862..824c8e47d05 100644 --- a/unit/interpreter/interpreter.cpp +++ b/unit/interpreter/interpreter.cpp @@ -17,6 +17,8 @@ Author: Diffblue Ltd. #include +#include + typedef interpretert::mp_vectort mp_vectort; class interpreter_testt @@ -46,7 +48,7 @@ SCENARIO("interpreter evaluation null pointer expressions") THEN("null pointer without operands") { unsignedbv_typet java_char(16); - pointer_typet pointer_type(java_char, 64); + pointer_typet pointer_type(java_char, sizeof(void *) * CHAR_BIT); null_pointer_exprt constant_expr{pointer_type}; @@ -56,13 +58,13 @@ SCENARIO("interpreter evaluation null pointer expressions") } THEN("null pointer with operands") { - pointer_typet outer_pointer_type(empty_typet(), 64); + pointer_typet outer_pointer_type(empty_typet(), sizeof(void *) * CHAR_BIT); constant_exprt outer_expression( "0000000000000000000000000000000000000000000000000000000000000000", outer_pointer_type); - outer_expression.add_to_operands( - null_pointer_exprt(pointer_typet(empty_typet(), 64))); + outer_expression.add_to_operands(null_pointer_exprt( + pointer_typet(empty_typet(), sizeof(void *) * CHAR_BIT))); mp_vectort mp_vector = interpreter_test.evaluate(outer_expression); diff --git a/unit/pointer-analysis/value_set.cpp b/unit/pointer-analysis/value_set.cpp index 81dafd11518..1e123a922d0 100644 --- a/unit/pointer-analysis/value_set.cpp +++ b/unit/pointer-analysis/value_set.cpp @@ -17,6 +17,8 @@ Author: Diffblue Ltd. #include #include +#include + static bool object_descriptor_matches( const exprt &descriptor_expr, const exprt &target) { @@ -49,8 +51,9 @@ SCENARIO( { // Create struct A { A *x; A *y } - struct_typet struct_A({{"x", pointer_typet(struct_tag_typet("A"), 64)}, - {"y", pointer_typet(struct_tag_typet("A"), 64)}}); + struct_typet struct_A( + {{"x", pointer_typet(struct_tag_typet("A"), sizeof(void *) * CHAR_BIT)}, + {"y", pointer_typet(struct_tag_typet("A"), sizeof(void *) * CHAR_BIT)}}); struct_A.set_tag("A"); auto &A_x = struct_A.components()[0]; @@ -225,7 +228,7 @@ SCENARIO( { // Make some global integers i1, i2, i3: signedbv_typet int32_type(32); - pointer_typet int32_ptr(int32_type, 64); + pointer_typet int32_ptr(int32_type, sizeof(void *) * CHAR_BIT); symbolt i1{"i1", int32_type, irep_idt{}}; i1.base_name = "i1"; diff --git a/unit/solvers/smt2_incremental/construct_value_expr_from_smt.cpp b/unit/solvers/smt2_incremental/construct_value_expr_from_smt.cpp index 630f4c64429..11a2ec1c2a4 100644 --- a/unit/solvers/smt2_incremental/construct_value_expr_from_smt.cpp +++ b/unit/solvers/smt2_incremental/construct_value_expr_from_smt.cpp @@ -103,14 +103,14 @@ TEST_CASE("Value expr construction from smt.", "[core][smt2_incremental]") rowt{smt_bit_vector_constant_termt{1, 8}, from_integer(1, c_bool_typet(8))}, rowt{ smt_bit_vector_constant_termt{0, 64}, - from_integer(0, pointer_typet(void_type(), 64 /* bits */))}, + from_integer(0, pointer_typet{empty_typet{}, 64 /* bits */})}, // The reason for the more intricate elaboration of a pointer with a value // of 12 is a limitation in the design of from_integer, which only handles // pointers with value 0 (null pointers). rowt{ smt_bit_vector_constant_termt{12, 64}, constant_exprt( - integer2bvrep(12, 64), pointer_typet(void_type(), 64 /* bits */))}, + integer2bvrep(12, 64), pointer_typet{empty_typet{}, 64 /* bits */})}, rowt{ smt_bit_vector_constant_termt{2, 42}, constant_exprt{"2", c_enum_tag_typet{enum_type_symbol.name}}}, @@ -184,7 +184,7 @@ TEST_CASE( "Unexpected conversion of exists quantifier to value expression."}, rowt{ smt_bit_vector_constant_termt{0, 16}, - pointer_typet{unsigned_int_type(), 0}, + pointer_typet{unsignedbv_typet{32}, 0}, "Width of smt bit vector term must match the width of pointer type"}, rowt{ smt_bit_vector_constant_termt{2, 42}, diff --git a/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp b/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp index e59f1ad6cbc..774cc68c5b4 100644 --- a/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp +++ b/unit/solvers/smt2_incremental/convert_expr_to_smt.cpp @@ -44,6 +44,8 @@ TEST_CASE("\"typet\" to smt sort conversion", "[core][smt2_incremental]") } } +// 32bit GCC defines i386 as a macro (with value 1) +#undef i386 enum class test_archt { i386, diff --git a/unit/util/lower_byte_operators.cpp b/unit/util/lower_byte_operators.cpp index 59c384b24c4..4f3ac9ba9be 100644 --- a/unit/util/lower_byte_operators.cpp +++ b/unit/util/lower_byte_operators.cpp @@ -279,7 +279,7 @@ SCENARIO("byte_extract_lowering", "[core][util][lowering][byte_extract]") signedbv_typet(128), ieee_float_spect::single_precision().to_type(), // generates the correct value, but remains wrapped in a typecast - // pointer_typet(u64, 64), + // pointer_typet(u64, sizeof(void *) * CHAR_BIT), vector_typet(size_type(), u8, size), vector_typet(size_type(), u64, size), complex_typet(s16), @@ -435,7 +435,7 @@ SCENARIO("byte_update_lowering", "[core][util][lowering][byte_update]") signedbv_typet(128), ieee_float_spect::single_precision().to_type(), // generates the correct value, but remains wrapped in a typecast - // pointer_typet(u64, 64), + // pointer_typet(u64, sizeof(void *) * CHAR_BIT), vector_typet(size_type(), u8, size), vector_typet(size_type(), u64, size), // complex_typet(s16),