Skip to content

Commit 56c3c76

Browse files
hannes-steffenhagen-diffbluehannes-steffenhagen-diffblue
authored
Merge pull request #5582 from hannes-steffenhagen-diffblue/usability/split-up-pointer-primitive-checks
Usability/split up pointer primitive checks
2 parents 7206654 + 0f8ac07 commit 56c3c76

File tree

6 files changed

+252
-156
lines changed

6 files changed

+252
-156
lines changed

‎regression/cbmc/pointer-extra-checks/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -8,8 +8,8 @@ main.c
88
^\[main.pointer_dereference.3\] .* dereference failure: pointer outside object bounds in \*q: SUCCESS$
99
^\[main.pointer_dereference.4\] .* dereference failure: deallocated dynamic object in \*r: SUCCESS$
1010
^\[main.pointer_dereference.5\] .* dereference failure: pointer outside dynamic object bounds in \*r: SUCCESS$
11-
^\[main.pointer_dereference.6\] .* dereference failure: pointer invalid in \*s: FAILURE$
12-
^\[main.pointer_dereference.7\] .* dereference failure: pointer NULL in \*s: FAILURE$
11+
^\[main.pointer_dereference.6\] .* dereference failure: pointer NULL in \*s: FAILURE$
12+
^\[main.pointer_dereference.7\] .* dereference failure: pointer invalid in \*s: FAILURE$
1313
^\[main.pointer_dereference.8\] .* dereference failure: deallocated dynamic object in \*s: FAILURE$
1414
^\[main.pointer_dereference.9\] .* dereference failure: dead object in \*s: FAILURE$
1515
^\[main.pointer_dereference.10\] .* dereference failure: pointer outside dynamic object bounds in \*s: FAILURE$

‎regression/cbmc/pointer-primitive-check-01/test.desc

Lines changed: 36 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,43 @@
1-
CORE
1+
CORE broken-smt-backend
22
main.c
33
--pointer-primitive-check
44
^EXIT=10$
55
^SIGNAL=0$
6-
\[main.pointer_primitives.1\] line \d+ pointer in pointer primitive is neither null nor valid in POINTER_OBJECT.*: FAILURE
7-
\[main.pointer_primitives.2\] line \d+ pointer in pointer primitive is neither null nor valid in POINTER_OFFSET.*: FAILURE
8-
\[main.pointer_primitives.3\] line \d+ pointer in pointer primitive is neither null nor valid in POINTER_OBJECT.*: FAILURE
9-
\[main.pointer_primitives.4\] line \d+ pointer in pointer primitive is neither null nor valid in OBJECT_SIZE.*: FAILURE
10-
\[main.pointer_primitives.5\] line \d+ pointer in pointer primitive is neither null nor valid in R_OK.*: FAILURE
11-
\[main.pointer_primitives.6\] line \d+ pointer in pointer primitive is neither null nor valid in W_OK.*: FAILURE
12-
\*\* 7 of \d+ failed
6+
\[main.pointer_primitives.1\] line \d+ pointer invalid in POINTER_OBJECT\(\(const void \*\)p1\): FAILURE
7+
\[main.pointer_primitives.2\] line \d+ deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p1\): SUCCESS
8+
\[main.pointer_primitives.3\] line \d+ dead object in POINTER_OBJECT\(\(const void \*\)p1\): SUCCESS
9+
\[main.pointer_primitives.4\] line \d+ pointer outside dynamic object bounds in POINTER_OBJECT\(\(const void \*\)p1\): FAILURE
10+
\[main.pointer_primitives.5\] line \d+ pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p1\): FAILURE
11+
\[main.pointer_primitives.6\] line \d+ pointer invalid in POINTER_OFFSET\(\(const void \*\)p2\): FAILURE
12+
\[main.pointer_primitives.7\] line \d+ deallocated dynamic object in POINTER_OFFSET\(\(const void \*\)p2\): SUCCESS
13+
\[main.pointer_primitives.8\] line \d+ dead object in POINTER_OFFSET\(\(const void \*\)p2\): SUCCESS
14+
\[main.pointer_primitives.9\] line \d+ pointer outside dynamic object bounds in POINTER_OFFSET\(\(const void \*\)p2\): FAILURE
15+
\[main.pointer_primitives.10\] line \d+ pointer outside object bounds in POINTER_OFFSET\(\(const void \*\)p2\): FAILURE
16+
\[main.pointer_primitives.11\] line \d+ pointer invalid in POINTER_OBJECT\(\(const void \*\)p3\): FAILURE
17+
\[main.pointer_primitives.12\] line \d+ deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p3\): SUCCESS
18+
\[main.pointer_primitives.13\] line \d+ dead object in POINTER_OBJECT\(\(const void \*\)p3\): SUCCESS
19+
\[main.pointer_primitives.14\] line \d+ pointer outside dynamic object bounds in POINTER_OBJECT\(\(const void \*\)p3\): FAILURE
20+
\[main.pointer_primitives.15\] line \d+ pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p3\): FAILURE
21+
\[main.pointer_primitives.16\] line \d+ pointer invalid in OBJECT_SIZE\(\(const void \*\)p4\): FAILURE
22+
\[main.pointer_primitives.17\] line \d+ deallocated dynamic object in OBJECT_SIZE\(\(const void \*\)p4\): SUCCESS
23+
\[main.pointer_primitives.18\] line \d+ dead object in OBJECT_SIZE\(\(const void \*\)p4\): SUCCESS
24+
\[main.pointer_primitives.19\] line \d+ pointer outside dynamic object bounds in OBJECT_SIZE\(\(const void \*\)p4\): FAILURE
25+
\[main.pointer_primitives.20\] line \d+ pointer outside object bounds in OBJECT_SIZE\(\(const void \*\)p4\): FAILURE
26+
\[main.pointer_primitives.21\] line \d+ pointer invalid in R_OK\(\(const void \*\)p5, \(__CPROVER_size_t\)1\): FAILURE
27+
\[main.pointer_primitives.22\] line \d+ deallocated dynamic object in R_OK\(\(const void \*\)p5, \(__CPROVER_size_t\)1\): SUCCESS
28+
\[main.pointer_primitives.23\] line \d+ dead object in R_OK\(\(const void \*\)p5, \(__CPROVER_size_t\)1\): SUCCESS
29+
\[main.pointer_primitives.24\] line \d+ pointer outside dynamic object bounds in R_OK\(\(const void \*\)p5, \(__CPROVER_size_t\)1\): FAILURE
30+
\[main.pointer_primitives.25\] line \d+ pointer outside object bounds in R_OK\(\(const void \*\)p5, \(__CPROVER_size_t\)1\): FAILURE
31+
\[main.pointer_primitives.26\] line \d+ pointer invalid in W_OK\(\(const void \*\)p6, \(__CPROVER_size_t\)1\): FAILURE
32+
\[main.pointer_primitives.27\] line \d+ deallocated dynamic object in W_OK\(\(const void \*\)p6, \(__CPROVER_size_t\)1\): SUCCESS
33+
\[main.pointer_primitives.28\] line \d+ dead object in W_OK\(\(const void \*\)p6, \(__CPROVER_size_t\)1\): SUCCESS
34+
\[main.pointer_primitives.29\] line \d+ pointer outside dynamic object bounds in W_OK\(\(const void \*\)p6, \(__CPROVER_size_t\)1\): FAILURE
35+
\[main.pointer_primitives.30\] line \d+ pointer outside object bounds in W_OK\(\(const void \*\)p6, \(__CPROVER_size_t\)1\): FAILURE
36+
\[main.pointer_primitives.31\] line \d+ pointer invalid in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): FAILURE
37+
\[main.pointer_primitives.32\] line \d+ deallocated dynamic object in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): SUCCESS
38+
\[main.pointer_primitives.33\] line \d+ dead object in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): SUCCESS
39+
\[main.pointer_primitives.34\] line \d+ pointer outside dynamic object bounds in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): FAILURE
40+
\[main.pointer_primitives.35\] line \d+ pointer outside object bounds in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): FAILURE
1341
--
1442
^warning: ignoring
1543
--

‎regression/cbmc/pointer-primitive-check-03/test.desc

Lines changed: 38 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -3,15 +3,45 @@ main.c
33
--pointer-primitive-check
44
^EXIT=10$
55
^SIGNAL=0$
6-
\[main.pointer_primitives.1\] line \d+ pointer in pointer primitive is neither null nor valid in POINTER_OBJECT.*: FAILURE
7-
\[main.pointer_primitives.2\] line \d+ pointer in pointer primitive is neither null nor valid in POINTER_OBJECT.*: FAILURE
8-
\[main.pointer_primitives.3\] line \d+ pointer in pointer primitive is neither null nor valid in POINTER_OBJECT.*: FAILURE
9-
\[main.pointer_primitives.4\] line \d+ pointer in pointer primitive is neither null nor valid in POINTER_OBJECT.*: FAILURE
10-
\[main.pointer_primitives.5\] line \d+ pointer in pointer primitive is neither null nor valid in POINTER_OBJECT.*: FAILURE
11-
\[main.pointer_primitives.6\] line \d+ pointer in pointer primitive is neither null nor valid in POINTER_OBJECT.*: FAILURE
12-
\[main.pointer_primitives.7\] line \d+ pointer in pointer primitive is neither null nor valid in POINTER_OBJECT.*: FAILURE
13-
\*\* 7 of \d+ failed
146
--
7+
\[main.pointer_primitives.1\] line \d+ pointer NULL in POINTER_OBJECT((const void \*)p1): SUCCESS
8+
\[main.pointer_primitives.2\] line \d+ pointer invalid in POINTER_OBJECT((const void \*)p1): FAILURE
9+
\[main.pointer_primitives.3\] line \d+ deallocated dynamic object in POINTER_OBJECT((const void \*)p1): SUCCESS
10+
\[main.pointer_primitives.4\] line \d+ dead object in POINTER_OBJECT((const void \*)p1): SUCCESS
11+
\[main.pointer_primitives.5\] line \d+ pointer outside dynamic object bounds in POINTER_OBJECT((const void \*)p1): FAILURE
12+
\[main.pointer_primitives.6\] line \d+ pointer outside object bounds in POINTER_OBJECT((const void \*)p1): FAILURE
13+
\[main.pointer_primitives.7\] line \d+ pointer NULL in POINTER_OBJECT((const void \*)p2): SUCCESS
14+
\[main.pointer_primitives.8\] line \d+ pointer invalid in POINTER_OBJECT((const void \*)p2): FAILURE
15+
\[main.pointer_primitives.9\] line \d+ deallocated dynamic object in POINTER_OBJECT((const void \*)p2): SUCCESS
16+
\[main.pointer_primitives.10\] line \d+ dead object in POINTER_OBJECT((const void \*)p2): SUCCESS
17+
\[main.pointer_primitives.11\] line \d+ pointer outside dynamic object bounds in POINTER_OBJECT((const void \*)p2): SUCCESS
18+
\[main.pointer_primitives.12\] line \d+ pointer outside object bounds in POINTER_OBJECT((const void \*)p2): FAILURE
19+
\[main.pointer_primitives.13\] line \d+ pointer NULL in POINTER_OBJECT((const void \*)p3): SUCCESS
20+
\[main.pointer_primitives.14\] line \d+ pointer invalid in POINTER_OBJECT((const void \*)p3): SUCCESS
21+
\[main.pointer_primitives.15\] line \d+ deallocated dynamic object in POINTER_OBJECT((const void \*)p3): SUCCESS
22+
\[main.pointer_primitives.16\] line \d+ dead object in POINTER_OBJECT((const void \*)p3): SUCCESS
23+
\[main.pointer_primitives.17\] line \d+ pointer outside dynamic object bounds in POINTER_OBJECT((const void \*)p3): FAILURE
24+
\[main.pointer_primitives.18\] line \d+ pointer outside object bounds in POINTER_OBJECT((const void \*)p3): FAILURE
25+
\[main.pointer_primitives.19\] line \d+ pointer NULL in POINTER_OBJECT((const void \*)p4): SUCCESS
26+
\[main.pointer_primitives.20\] line \d+ pointer invalid in POINTER_OBJECT((const void \*)p4): SUCCESS
27+
\[main.pointer_primitives.21\] line \d+ deallocated dynamic object in POINTER_OBJECT((const void \*)p4): SUCCESS
28+
\[main.pointer_primitives.22\] line \d+ dead object in POINTER_OBJECT((const void \*)p4): SUCCESS
29+
\[main.pointer_primitives.23\] line \d+ pointer outside dynamic object bounds in POINTER_OBJECT((const void \*)p4): FAILURE
30+
\[main.pointer_primitives.24\] line \d+ pointer outside object bounds in POINTER_OBJECT((const void \*)p4): SUCCESS
31+
\[main.pointer_primitives.25\] line \d+ pointer NULL in POINTER_OBJECT((const void \*)p5): SUCCESS
32+
\[main.pointer_primitives.26\] line \d+ pointer invalid in POINTER_OBJECT((const void \*)p5): SUCCESS
33+
\[main.pointer_primitives.27\] line \d+ deallocated dynamic object in POINTER_OBJECT((const void \*)p5): SUCCESS
34+
\[main.pointer_primitives.28\] line \d+ dead object in POINTER_OBJECT((const void \*)p5): SUCCESS
35+
\[main.pointer_primitives.29\] line \d+ pointer outside dynamic object bounds in POINTER_OBJECT((const void \*)p5): FAILURE
36+
\[main.pointer_primitives.30\] line \d+ pointer outside object bounds in POINTER_OBJECT((const void \*)p5): SUCCESS
37+
\[main.pointer_primitives.31\] line \d+ dead object in POINTER_OBJECT((const void \*)p6): FAILURE
38+
\[main.pointer_primitives.32\] line \d+ pointer outside object bounds in POINTER_OBJECT((const void \*)p6): SUCCESS
39+
\[main.pointer_primitives.33\] line \d+ pointer NULL in POINTER_OBJECT((const void \*)p7): SUCCESS
40+
\[main.pointer_primitives.34\] line \d+ pointer invalid in POINTER_OBJECT((const void \*)p7): SUCCESS
41+
\[main.pointer_primitives.35\] line \d+ deallocated dynamic object in POINTER_OBJECT((const void \*)p7): FAILURE
42+
\[main.pointer_primitives.36\] line \d+ dead object in POINTER_OBJECT((const void \*)p7): SUCCESS
43+
\[main.pointer_primitives.37\] line \d+ pointer outside dynamic object bounds in POINTER_OBJECT((const void \*)p7): SUCCESS
44+
\[main.pointer_primitives.38\] line \d+ pointer outside object bounds in POINTER_OBJECT((const void \*)p7): SUCCESS
1545
^warning: ignoring
1646
--
1747
Verifies that the pointer primitives check fails for the various forms of

‎regression/cbmc/pointer-primitive-check-04/test.desc

Lines changed: 6 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,13 @@
1-
CORE
1+
CORE broken-smt-backend
22
main.c
33
--pointer-primitive-check
44
^EXIT=10$
55
^SIGNAL=0$
6-
\[main.pointer_primitives.1\] line \d+ pointer in pointer primitive is neither null nor valid in R_OK.*: FAILURE
7-
\*\* 1 of \d+ failed
6+
\[main.pointer_primitives.1\] line \d+ pointer invalid in R_OK\(\(const void \*\)p, \(__CPROVER_size_t\)1\): FAILURE
7+
\[main.pointer_primitives.2\] line \d+ deallocated dynamic object in R_OK\(\(const void \*\)p, \(__CPROVER_size_t\)1\): SUCCESS
8+
\[main.pointer_primitives.3\] line \d+ dead object in R_OK\(\(const void \*\)p, \(__CPROVER_size_t\)1\): SUCCESS
9+
\[main.pointer_primitives.4\] line \d+ pointer outside dynamic object bounds in R_OK\(\(const void \*\)p, \(__CPROVER_size_t\)1\): FAILURE
10+
\[main.pointer_primitives.5\] line \d+ pointer outside object bounds in R_OK\(\(const void \*\)p, \(__CPROVER_size_t\)1\): FAILURE
811
--
912
^warning: ignoring
1013
--

‎regression/goto-harness/pointer-to-array-function-parameters-with-size/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,8 @@ test.c
33
--harness-type call-function --function test --treat-pointer-as-array arr --associated-array-size arr:sz
44
^EXIT=0$
55
^SIGNAL=0$
6-
\[test.pointer_dereference.1\] line \d+ dereference failure: pointer invalid in arr\[\(signed( long)* int\)i\]: SUCCESS
7-
\[test.pointer_dereference.2\] line \d+ dereference failure: pointer NULL in arr\[\(signed( long)* int\)i\]: SUCCESS
6+
\[test.pointer_dereference.1\] line \d+ dereference failure: pointer NULL in arr\[\(signed( long)* int\)i\]: SUCCESS
7+
\[test.pointer_dereference.2\] line \d+ dereference failure: pointer invalid in arr\[\(signed( long)* int\)i\]: SUCCESS
88
\[test.pointer_dereference.3\] line \d+ dereference failure: deallocated dynamic object in arr\[\(signed( long)* int\)i\]: SUCCESS
99
\[test.pointer_dereference.4\] line \d+ dereference failure: dead object in arr\[\(signed( long)* int\)i\]: SUCCESS
1010
\[test.pointer_dereference.5\] line \d+ dereference failure: pointer outside dynamic object bounds in arr\[\(signed( long)* int\)i\]: SUCCESS

0 commit comments

Comments
 (0)