Skip to content

Commit 74bb276

Browse files
kroeningkroening
authored
Merge pull request #7756 from tautschnig/bugfixes/32-bit
Test 32-bit builds in CI and fix platform-specific code and tests
2 parents c46b822 + 1a30ad4 commit 74bb276

File tree

147 files changed

+561
-429
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

147 files changed

+561
-429
lines changed

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

Lines changed: 46 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -442,6 +442,52 @@ jobs:
442442
- name: Run tests
443443
run: cd build; ctest . -V -L CORE -j2
444444

445+
# This job takes approximately 30 to 60 minutes
446+
check-ubuntu-22_04-cmake-gcc-32bit:
447+
runs-on: ubuntu-22.04
448+
steps:
449+
- uses: actions/checkout@v3
450+
with:
451+
submodules: recursive
452+
- name: Fetch dependencies
453+
env:
454+
# This is needed in addition to -yq to prevent apt-get from asking for
455+
# user input
456+
DEBIAN_FRONTEND: noninteractive
457+
run: |
458+
sudo apt-get update
459+
sudo apt-get install --no-install-recommends -yq cmake ninja-build gcc gdb g++ maven flex bison libxml2-utils ccache doxygen z3 g++-multilib
460+
- name: Confirm z3 solver is available and log the version installed
461+
run: z3 --version
462+
- name: Download cvc-5 from the releases page and make sure it can be deployed
463+
run: |
464+
wget -O cvc5 https://github.com/cvc5/cvc5/releases/download/cvc5-${{env.cvc5-version}}/cvc5-Linux
465+
chmod u+x cvc5
466+
mv cvc5 /usr/local/bin
467+
cvc5 --version
468+
- name: Prepare ccache
469+
uses: actions/cache@v3
470+
with:
471+
path: .ccache
472+
key: ${{ runner.os }}-22.04-Release-32-${{ github.ref }}-${{ github.sha }}-PR
473+
restore-keys: |
474+
${{ runner.os }}-22.04-Release-32-${{ github.ref }}
475+
${{ runner.os }}-22.04-Release-32
476+
- name: ccache environment
477+
run: |
478+
echo "CCACHE_BASEDIR=$PWD" >> $GITHUB_ENV
479+
echo "CCACHE_DIR=$PWD/.ccache" >> $GITHUB_ENV
480+
- name: Configure using CMake
481+
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
482+
- name: Zero ccache stats and limit in size
483+
run: ccache -z --max-size=500M
484+
- name: Build with Ninja
485+
run: ninja -C build -j2
486+
- name: Print ccache stats
487+
run: ccache -s
488+
- name: Run tests
489+
run: cd build; ctest . -V -L CORE -j2
490+
445491
# This job takes approximately 5 to 24 minutes
446492
check-ubuntu-20_04-cmake-gcc-KNOWNBUG:
447493
runs-on: ubuntu-20.04

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ array_write.c
33
--trace
44
Passing problem to incremental SMT2 solving
55
^Trace for main\.assertion\.2
6-
example_array\[\d{1,4}ll?\]=42
6+
example_array\[\d{1,4}l?l?\]=42
77
^EXIT=10$
88
^SIGNAL=0$
99
--

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -4,9 +4,9 @@ enum_in_array.c
44
Passing problem to incremental SMT2 solving
55
line 18 Array at index 0 is V0, so this should fail: FAILURE
66
i=0u \(00000000 00000000 00000000 00000000\)
7-
e\[0l+\]=/\*enum\*/V0 \(00000000 00000000 00000000 00000000\)
8-
e\[1l+\]=/\*enum\*/V1 \(00000000 00000000 00000000 00000001\)
9-
e\[2l+\]=/\*enum\*/V2 \(00000000 00000000 00000000 00000010\)
7+
e\[0l*\]=/\*enum\*/V0 \(00000000 00000000 00000000 00000000\)
8+
e\[1l*\]=/\*enum\*/V1 \(00000000 00000000 00000000 00000001\)
9+
e\[2l*\]=/\*enum\*/V2 \(00000000 00000000 00000000 00000010\)
1010
^EXIT=10$
1111
^SIGNAL=0$
1212
--

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -4,13 +4,13 @@ test.c
44
Starting Bounded Model Checking
55
^\(set-option :produce-models true\)$
66
^\(set-logic ALL\)$
7-
^\(declare-fun size_of_object \(\(_ BitVec 8\)\) \(_ BitVec 64\)\)$
7+
^\(declare-fun size_of_object \(\(_ BitVec 8\)\) \(_ BitVec \d+\)\)$
88
^Passing problem to incremental SMT2 solving via SMT2 incremental dry-run$
99
^\(define-fun B0 \(\) Bool true\)$
1010
^\(define-fun B2 \(\) Bool \(not false\)\)$
1111
^\(assert B2\)$
12-
^\(assert \(= \(size_of_object \(_ bv1 8\)\) \(_ bv0 64\)\)\)$
13-
^\(assert \(= \(size_of_object \(_ bv0 8\)\) \(_ bv0 64\)\)\)$
12+
^\(assert \(= \(size_of_object \(_ bv1 8\)\) \(_ bv0 \d+\)\)\)$
13+
^\(assert \(= \(size_of_object \(_ bv0 8\)\) \(_ bv0 \d+\)\)\)$
1414
^\(check-sat\)$
1515
^EXIT=0$
1616
^SIGNAL=0$

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

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,6 @@ int main()
1616
}
1717

1818
__CPROVER_assume(y >= z);
19-
__CPROVER_assert(x != y, "x != y: expected successful");
2019
__CPROVER_assert(x == y, "x == y: expected failure");
2120

2221
__CPROVER_assume(z >= x);

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

Lines changed: 4 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,11 +1,10 @@
11
CORE
22
pointers_assume.c
33
--trace
4-
\[main\.assertion\.1\] line \d+ x != y: expected successful: SUCCESS
5-
\[main\.assertion\.2\] line \d+ x == y: expected failure: FAILURE
6-
\[main\.assertion\.3\] line \d+ z >= x: expected successful: SUCCESS
7-
\[main\.assertion\.4\] line \d+ z <= y: expected successful: SUCCESS
8-
\[main\.assertion\.5\] line \d+ z <= x: expected failure: FAILURE
4+
\[main\.assertion\.1\] line \d+ x == y: expected failure: FAILURE
5+
\[main\.assertion\.2\] line \d+ z >= x: expected successful: SUCCESS
6+
\[main\.assertion\.3\] line \d+ z <= y: expected successful: SUCCESS
7+
\[main\.assertion\.4\] line \d+ z <= x: expected failure: FAILURE
98
^EXIT=10$
109
^SIGNAL=0$
1110
--

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -5,9 +5,9 @@ line 12 Expected int sizes\.: SUCCESS
55
line 13 Size is always 2\. \(Can be disproved\.\): FAILURE
66
line 14 Size is always 4\. \(Can be disproved\.\): FAILURE
77
line 16 Size of NULL\.: FAILURE
8-
size=2ul
9-
size=4ul
10-
null_size=0ul
8+
size=2ul*
9+
size=4ul*
10+
null_size=0ul*
1111
^EXIT=10$
1212
^SIGNAL=0$
1313
--

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ line 17 assertion struct_array\[x\]\.eggs \+ struct_array\[x\]\.ham != 11\: FAIL
99
\{\s*\.eggs=\d+,\s*\.ham=7\s*\}
1010
\{\s*\.eggs=\d+,\s*\.ham=8\s*\}
1111
x=\d{1,4}\s
12-
struct_array\[\(signed (long )+int\)x\]\.eggs=3
12+
struct_array\[(\(signed (long )+int\))?x\]\.eggs=3
1313
--
1414
--
1515
This test covers support for examples with large arrays of structs using nondet

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,7 @@ int main()
1313

1414
__CPROVER_assume(fd >= 0);
1515
__CPROVER_assume(nbytes < SIZE);
16+
__CPROVER_assume(fd <= SSIZE_MAX / sizeof(struct __CPROVER_pipet));
1617

1718
write(fd, ptr, nbytes);
1819
}

‎regression/cbmc-primitives/exists_memory_checks/invalid_index_range.desc

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

‎regression/cbmc-primitives/exists_memory_checks/negated_exists.desc

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

‎regression/cbmc-primitives/exists_memory_checks/smt_missing_range_check.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ smt_missing_range_check.c
55
^SIGNAL=0$
66
^VERIFICATION FAILED$
77
\[main\.assertion\.1\] line \d assertion __CPROVER_exists \{ int i; a\[i\] == i \*i \}: SUCCESS
8-
\[main\.pointer_dereference\.11\] line \d dereference failure: pointer outside object bounds in a\[\(signed (long|long long) int\)i\]: FAILURE
8+
\[main\.pointer_dereference\.11\] line \d dereference failure: pointer outside object bounds in a\[(\(signed (long|long long) int\))?i\]: FAILURE
99
--
1010
--
1111
Check that memory checks fail for pointer dereferences inside an existential

‎regression/cbmc-primitives/exists_memory_checks/valid_index_range.desc

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

‎regression/cbmc-primitives/forall_6231_1/test.desc

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

‎regression/cbmc-primitives/forall_6231_2/test.desc

Lines changed: 12 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -4,19 +4,19 @@ test.c
44
^EXIT=0$
55
^SIGNAL=0$
66
\[main\.assertion\.1\] line \d+ assertion __CPROVER_forall \{ int i ; \(0 <= i && i < 1\) ==> \*\(a\+i\) == \*\(a\+i\) \}: SUCCESS
7-
\[main\.pointer_dereference\.1\] line \d+ dereference failure: pointer NULL in a\[\(signed (long|long long) int\)i\]: SUCCESS
8-
\[main\.pointer_dereference\.2\] line \d+ dereference failure: pointer invalid in a\[\(signed (long|long long) int\)i\]: SUCCESS
9-
\[main\.pointer_dereference\.3\] line \d+ dereference failure: deallocated dynamic object in a\[\(signed (long|long long) int\)i\]: SUCCESS
10-
\[main\.pointer_dereference\.4\] line \d+ dereference failure: dead object in a\[\(signed (long|long long) int\)i\]: SUCCESS
11-
\[main\.pointer_dereference\.5\] line \d+ dereference failure: pointer outside object bounds in a\[\(signed (long|long long) int\)i\]: SUCCESS
12-
\[main\.pointer_dereference\.6\] line \d+ dereference failure: invalid integer address in a\[\(signed (long|long long) int\)i\]: SUCCESS
7+
\[main\.pointer_dereference\.1\] line \d+ dereference failure: pointer NULL in a\[(\(signed (long|long long) int\))?i\]: SUCCESS
8+
\[main\.pointer_dereference\.2\] line \d+ dereference failure: pointer invalid in a\[(\(signed (long|long long) int\))?i\]: SUCCESS
9+
\[main\.pointer_dereference\.3\] line \d+ dereference failure: deallocated dynamic object in a\[(\(signed (long|long long) int\))?i\]: SUCCESS
10+
\[main\.pointer_dereference\.4\] line \d+ dereference failure: dead object in a\[(\(signed (long|long long) int\))?i\]: SUCCESS
11+
\[main\.pointer_dereference\.5\] line \d+ dereference failure: pointer outside object bounds in a\[(\(signed (long|long long) int\))?i\]: SUCCESS
12+
\[main\.pointer_dereference\.6\] line \d+ dereference failure: invalid integer address in a\[(\(signed (long|long long) int\))?i\]: SUCCESS
1313
\[main\.assertion.2] line \d+ assertion __CPROVER_forall \{ int j; \!\(0 <= j && j < 1\) || \(j == 0 && \*\(a\+j\) == \*\(a+j\)\) \}: SUCCESS
14-
\[main\.pointer_dereference\.7] line \d+ dereference failure: pointer NULL in a\[\(signed (long|long long) int\)j\]: SUCCESS
15-
\[main\.pointer_dereference\.8] line \d+ dereference failure: pointer invalid in a\[\(signed (long|long long) int\)j\]: SUCCESS
16-
\[main\.pointer_dereference\.9] line \d+ dereference failure: deallocated dynamic object in a\[\(signed (long|long long) int\)j\]: SUCCESS
17-
\[main\.pointer_dereference\.10] line \d+ dereference failure: dead object in a\[\(signed (long|long long) int\)j\]: SUCCESS
18-
\[main\.pointer_dereference\.11] line \d+ dereference failure: pointer outside object bounds in a\[\(signed (long|long long) int\)j\]: SUCCESS
19-
\[main\.pointer_dereference\.12] line \d+ dereference failure: invalid integer address in a\[\(signed (long|long long) int\)j\]: SUCCESS
14+
\[main\.pointer_dereference\.7] line \d+ dereference failure: pointer NULL in a\[(\(signed (long|long long) int\))?j\]: SUCCESS
15+
\[main\.pointer_dereference\.8] line \d+ dereference failure: pointer invalid in a\[(\(signed (long|long long) int\))?j\]: SUCCESS
16+
\[main\.pointer_dereference\.9] line \d+ dereference failure: deallocated dynamic object in a\[(\(signed (long|long long) int\))?j\]: SUCCESS
17+
\[main\.pointer_dereference\.10] line \d+ dereference failure: dead object in a\[(\(signed (long|long long) int\))?j\]: SUCCESS
18+
\[main\.pointer_dereference\.11] line \d+ dereference failure: pointer outside object bounds in a\[(\(signed (long|long long) int\))?j\]: SUCCESS
19+
\[main\.pointer_dereference\.12] line \d+ dereference failure: invalid integer address in a\[(\(signed (long|long long) int\))?j\]: SUCCESS
2020
^VERIFICATION SUCCESSFUL$
2121
--
2222
--

‎regression/cbmc-primitives/forall_6231_3/test.desc

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

‎regression/cbmc-primitives/forall_6231_3/test_malloc_less_than_bound.desc

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

‎regression/cbmc/Pointer2/main.c

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
11
int main()
22
{
33
int x;
4-
unsigned long long x_i;
4+
__CPROVER_size_t x_i;
55
_Static_assert(sizeof(&x) == sizeof(x_i), "pointer width");
6-
__CPROVER_assert(((unsigned long long)&x & 0x1ULL) == 0, "LSB is zero");
7-
x_i = (unsigned long long)&x >> 1;
6+
__CPROVER_assert(((__CPROVER_size_t)&x & 0x1ULL) == 0, "LSB is zero");
7+
x_i = (__CPROVER_size_t)&x >> 1;
88
x_i <<= 1;
99
__CPROVER_assert(*(int *)x_i == x, "pointer to x is tracked through shifts");
1010
}

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE new-smt-backend
22
test.c
33
--show-vcc
4-
main::1::array!0@1#2 = with\(main::1::array!0@1#1, cast\(main::argc!0@1#1 \+ -1, signedbv\[64\]\), 1\)
4+
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\)
55
main::1::array!0@1#3 = with\(main::1::array!0@1#2, 1, main::argc!0@1#1\)
66
^EXIT=0$
77
^SIGNAL=0$

0 commit comments

Comments
 (0)