Skip to content

Commit 4a6be48

Browse files
tautschnigtautschnig
committed
Make pointer-primitive-check a no-op when behaviour is always defined
pointer_object, pointer_offset have well-defined behaviour even when the input is an unconstrained pointer: the result is equally unconstrained. Regression tests are updated to reflect the reduced number of checks generated by --pointer-primitive-check. Note that the patterns in pointer-primitive-check-03 never were effective as they were placed in the patterns-not-to-seen section of test.desc while also missing proper parenthesis escaping (making the patterns trivially non-matching).
1 parent 7eceeb5 commit 4a6be48

File tree

15 files changed

+122
-199
lines changed

15 files changed

+122
-199
lines changed

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

Lines changed: 30 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -3,35 +3,36 @@ main.c
33
--pointer-primitive-check
44
^EXIT=10$
55
^SIGNAL=0$
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 object bounds in POINTER_OBJECT\(\(const void \*\)p1\): FAILURE
10-
\[main.pointer_primitives.5\] line \d+ pointer invalid in POINTER_OFFSET\(\(const void \*\)p2\): FAILURE
11-
\[main.pointer_primitives.6\] line \d+ deallocated dynamic object in POINTER_OFFSET\(\(const void \*\)p2\): SUCCESS
12-
\[main.pointer_primitives.7\] line \d+ dead object in POINTER_OFFSET\(\(const void \*\)p2\): SUCCESS
13-
\[main.pointer_primitives.8\] line \d+ pointer outside object bounds in POINTER_OFFSET\(\(const void \*\)p2\): FAILURE
14-
\[main.pointer_primitives.9\] line \d+ pointer invalid in POINTER_OBJECT\(\(const void \*\)p3\): FAILURE
15-
\[main.pointer_primitives.10\] line \d+ deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p3\): SUCCESS
16-
\[main.pointer_primitives.11\] line \d+ dead object in POINTER_OBJECT\(\(const void \*\)p3\): SUCCESS
17-
\[main.pointer_primitives.12\] line \d+ pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p3\): FAILURE
18-
\[main.pointer_primitives.13\] line \d+ pointer invalid in OBJECT_SIZE\(\(const void \*\)p4\): FAILURE
19-
\[main.pointer_primitives.14\] line \d+ deallocated dynamic object in OBJECT_SIZE\(\(const void \*\)p4\): SUCCESS
20-
\[main.pointer_primitives.15\] line \d+ dead object in OBJECT_SIZE\(\(const void \*\)p4\): SUCCESS
21-
\[main.pointer_primitives.16\] line \d+ pointer outside object bounds in OBJECT_SIZE\(\(const void \*\)p4\): FAILURE
22-
\[main.pointer_primitives.17\] line \d+ pointer invalid in R_OK\(p5, .*1\): FAILURE
23-
\[main.pointer_primitives.18\] line \d+ deallocated dynamic object in R_OK\(p5, .*1\): SUCCESS
24-
\[main.pointer_primitives.19\] line \d+ dead object in R_OK\(p5, .*1\): SUCCESS
25-
\[main.pointer_primitives.20\] line \d+ pointer outside object bounds in R_OK\(p5, .*1\): FAILURE
26-
\[main.pointer_primitives.21\] line \d+ pointer invalid in W_OK\(p6, \(.*\)1\): FAILURE
27-
\[main.pointer_primitives.22\] line \d+ deallocated dynamic object in W_OK\(p6, .*1\): SUCCESS
28-
\[main.pointer_primitives.23\] line \d+ dead object in W_OK\(p6, .*1\): SUCCESS
29-
\[main.pointer_primitives.24\] line \d+ pointer outside object bounds in W_OK\(p6, .*1\): FAILURE
30-
\[main.pointer_primitives.25\] line \d+ pointer invalid in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): FAILURE
31-
\[main.pointer_primitives.26\] line \d+ deallocated dynamic object in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): SUCCESS
32-
\[main.pointer_primitives.27\] line \d+ dead object in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): SUCCESS
33-
\[main.pointer_primitives.28\] line \d+ pointer outside object bounds in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): FAILURE
6+
\[main.pointer_primitives.\d+\] line \d+ pointer invalid in OBJECT_SIZE\(\(const void \*\)p4\): FAILURE
7+
\[main.pointer_primitives.\d+\] line \d+ deallocated dynamic object in OBJECT_SIZE\(\(const void \*\)p4\): SUCCESS
8+
\[main.pointer_primitives.\d+\] line \d+ dead object in OBJECT_SIZE\(\(const void \*\)p4\): SUCCESS
9+
\[main.pointer_primitives.\d+\] line \d+ pointer outside object bounds in OBJECT_SIZE\(\(const void \*\)p4\): FAILURE
10+
\[main.pointer_primitives.\d+\] line \d+ pointer invalid in R_OK\(p5, .*1\): FAILURE
11+
\[main.pointer_primitives.\d+\] line \d+ deallocated dynamic object in R_OK\(p5, .*1\): SUCCESS
12+
\[main.pointer_primitives.\d+\] line \d+ dead object in R_OK\(p5, .*1\): SUCCESS
13+
\[main.pointer_primitives.\d+\] line \d+ pointer outside object bounds in R_OK\(p5, .*1\): FAILURE
14+
\[main.pointer_primitives.\d+\] line \d+ pointer invalid in W_OK\(p6, \(.*\)1\): FAILURE
15+
\[main.pointer_primitives.\d+\] line \d+ deallocated dynamic object in W_OK\(p6, .*1\): SUCCESS
16+
\[main.pointer_primitives.\d+\] line \d+ dead object in W_OK\(p6, .*1\): SUCCESS
17+
\[main.pointer_primitives.\d+\] line \d+ pointer outside object bounds in W_OK\(p6, .*1\): FAILURE
18+
\[main.pointer_primitives.\d+\] line \d+ pointer invalid in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): FAILURE
19+
\[main.pointer_primitives.\d+\] line \d+ deallocated dynamic object in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): SUCCESS
20+
\[main.pointer_primitives.\d+\] line \d+ dead object in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): SUCCESS
21+
\[main.pointer_primitives.\d+\] line \d+ pointer outside object bounds in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): FAILURE
3422
--
3523
^warning: ignoring
24+
\[main.pointer_primitives\.\d+\] line \d+ pointer invalid in POINTER_OBJECT\(\(const void \*\)p1\): FAILURE
25+
\[main.pointer_primitives\.\d+\] line \d+ deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p1\): SUCCESS
26+
\[main.pointer_primitives\.\d+\] line \d+ dead object in POINTER_OBJECT\(\(const void \*\)p1\): SUCCESS
27+
\[main.pointer_primitives\.\d+\] line \d+ pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p1\): FAILURE
28+
\[main.pointer_primitives\.\d+\] line \d+ pointer invalid in POINTER_OFFSET\(\(const void \*\)p2\): FAILURE
29+
\[main.pointer_primitives\.\d+\] line \d+ deallocated dynamic object in POINTER_OFFSET\(\(const void \*\)p2\): SUCCESS
30+
\[main.pointer_primitives\.\d+\] line \d+ dead object in POINTER_OFFSET\(\(const void \*\)p2\): SUCCESS
31+
\[main.pointer_primitives\.\d+\] line \d+ pointer outside object bounds in POINTER_OFFSET\(\(const void \*\)p2\): FAILURE
32+
\[main.pointer_primitives\.\d+\] line \d+ pointer invalid in POINTER_OBJECT\(\(const void \*\)p3\): FAILURE
33+
\[main.pointer_primitives\.\d+\] line \d+ deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p3\): SUCCESS
34+
\[main.pointer_primitives\.\d+\] line \d+ dead object in POINTER_OBJECT\(\(const void \*\)p3\): SUCCESS
35+
\[main.pointer_primitives\.\d+\] line \d+ pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p3\): FAILURE
3636
--
37-
Verifies that checks are added for all pointer primitives
37+
Verifies that checks are added for exactly those pointer primitives that are not
38+
universally well defined.

‎regression/cbmc/pointer-primitive-check-02/main.c

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -4,8 +4,8 @@ char *p1;
44

55
void main()
66
{
7-
__CPROVER_POINTER_OBJECT(p1);
7+
__CPROVER_r_ok(p1, 1);
88

99
char *p2 = NULL;
10-
__CPROVER_POINTER_OBJECT(p2);
10+
__CPROVER_r_ok(p2, 1);
1111
}

‎regression/cbmc/pointer-primitive-check-03/main.c

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -4,37 +4,37 @@ void main()
44
{
55
// uninitialized pointer
66
char *p1;
7-
__CPROVER_POINTER_OBJECT(p1);
7+
__CPROVER_r_ok(p1, 1);
88

99
// special value of invalid pointer
1010
char *p2 = (size_t)1 << (sizeof(char *) * 8 - 8);
11-
__CPROVER_POINTER_OBJECT(p2);
11+
__CPROVER_r_ok(p2, 1);
1212

1313
// pointer object 123, offset 123, not pointing to valid memory
1414
char *p3 = ((size_t)123 << (sizeof(char *) * 8 - 8)) | 123;
15-
__CPROVER_POINTER_OBJECT(p3);
15+
__CPROVER_r_ok(p3, 1);
1616

1717
// negative offset
1818
char *p4 = malloc(1);
1919
p4 -= 1;
20-
__CPROVER_POINTER_OBJECT(p4);
20+
__CPROVER_r_ok(p4, 1);
2121

2222
// offset out of bounds
2323
char *p5 = malloc(10);
2424
p5 += 10;
25-
__CPROVER_POINTER_OBJECT(p5);
25+
__CPROVER_r_ok(p5, 1);
2626

2727
// dead
2828
char *p6;
2929
{
3030
char c;
3131
p6 = &c;
3232
}
33-
__CPROVER_POINTER_OBJECT(p6);
33+
__CPROVER_r_ok(p6, 1);
3434
*p6;
3535

3636
// deallocated
3737
char *p7 = malloc(1);
3838
free(p7);
39-
__CPROVER_POINTER_OBJECT(p7);
39+
__CPROVER_r_ok(p7, 1);
4040
}

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

Lines changed: 7 additions & 38 deletions
Original file line numberDiff line numberDiff line change
@@ -3,45 +3,14 @@ main.c
33
--pointer-primitive-check
44
^EXIT=10$
55
^SIGNAL=0$
6+
^\[main.pointer_primitives.\d+\] line 7 .* in R_OK\(p1, \(unsigned (long (long )?)?int\)1\): FAILURE$
7+
^\[main.pointer_primitives.\d+\] line 11 .* in R_OK\(p2, \(unsigned (long (long )?)?int\)1\): FAILURE$
8+
^\[main.pointer_primitives.\d+\] line 15 .* in R_OK\(p3, \(unsigned (long (long )?)?int\)1\): FAILURE$
9+
^\[main.pointer_primitives.\d+\] line 20 .* in R_OK\(p4, \(unsigned (long (long )?)?int\)1\): FAILURE$
10+
^\[main.pointer_primitives.\d+\] line 25 .* in R_OK\(p5, \(unsigned (long (long )?)?int\)1\): FAILURE$
11+
^\[main.pointer_primitives.\d+\] line 33 .* in R_OK\(p6, \(unsigned (long (long )?)?int\)1\): FAILURE$
12+
^\[main.pointer_primitives.\d+\] line 39 .* in R_OK\(p7, \(unsigned (long (long )?)?int\)1\): FAILURE$
613
--
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
4514
^warning: ignoring
4615
--
4716
Verifies that the pointer primitives check fails for the various forms of

‎regression/cbmc/pragma_cprover3/main.c

Lines changed: 8 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -8,13 +8,19 @@ int main()
88
#pragma CPROVER check push
99
#pragma CPROVER check disable "pointer-primitive"
1010
// do not generate checks for the following statements
11-
if(__CPROVER_same_object(p, q))
11+
if(__CPROVER_r_ok(p, sizeof(*p) + 2))
1212
{
1313
}
1414
#pragma CPROVER check pop
1515

16-
// generate check and fail on the following statements
16+
// no checks are generated for the following statement as the behaviour is
17+
// always defined
1718
if(__CPROVER_same_object(p, q))
1819
{
1920
}
21+
22+
// generate check and fail on the following statements
23+
if(__CPROVER_r_ok(q, 1))
24+
{
25+
}
2026
}

‎regression/cbmc/pragma_cprover3/test.desc

Lines changed: 5 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -2,15 +2,12 @@ CORE
22
main.c
33
--pointer-primitive-check
44
^main.c function main$
5-
^\[main.pointer_primitives.\d+\] line 17 pointer invalid in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$
6-
^\[main.pointer_primitives.\d+\] line 17 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$
7-
^\[main.pointer_primitives.\d+\] line 17 dead object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$
8-
^\[main.pointer_primitives.\d+\] line 17 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$
9-
^\[main.pointer_primitives.\d+\] line 17 pointer invalid in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$
10-
^\[main.pointer_primitives.\d+\] line 17 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$
11-
^\[main.pointer_primitives.\d+\] line 17 dead object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$
12-
^\[main.pointer_primitives.\d+\] line 17 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$
5+
^\[main.pointer_primitives.\d+\] line 23 pointer invalid in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$
6+
^\[main.pointer_primitives.\d+\] line 23 pointer outside object bounds in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$
137
^VERIFICATION FAILED$
148
^EXIT=10$
159
^SIGNAL=0$
1610
--
11+
^\[main.pointer_primitives.\d+\] line 11
12+
^\[main.pointer_primitives.\d+\] line 18
13+
--

‎regression/cbmc/pragma_cprover_enable3/main.c

Lines changed: 3 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,20 +1,17 @@
1-
#include <stdlib.h>
2-
31
int main()
42
{
5-
char *p = malloc(sizeof(*p));
6-
char *q;
3+
char *p, *q;
74

85
#pragma CPROVER check push
96
#pragma CPROVER check enable "pointer-primitive"
107
// generate checks for the following statements and fail
11-
if(__CPROVER_same_object(p, q))
8+
if(__CPROVER_r_ok(p, 1))
129
{
1310
}
1411
#pragma CPROVER check pop
1512

1613
// but do not generate checks on the following statements
17-
if(__CPROVER_same_object(p, q))
14+
if(__CPROVER_r_ok(q, 1))
1815
{
1916
}
2017
}

‎regression/cbmc/pragma_cprover_enable3/test.desc

Lines changed: 3 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -2,17 +2,11 @@ CORE
22
main.c
33

44
^main.c function main$
5-
^\[main.pointer_primitives.\d+\] line 11 pointer invalid in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$
6-
^\[main.pointer_primitives.\d+\] line 11 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$
7-
^\[main.pointer_primitives.\d+\] line 11 dead object in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$
8-
^\[main.pointer_primitives.\d+\] line 11 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)p\): SUCCESS$
9-
^\[main.pointer_primitives.\d+\] line 11 pointer invalid in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$
10-
^\[main.pointer_primitives.\d+\] line 11 deallocated dynamic object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$
11-
^\[main.pointer_primitives.\d+\] line 11 dead object in POINTER_OBJECT\(\(const void \*\)q\): SUCCESS$
12-
^\[main.pointer_primitives.\d+\] line 11 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)q\): FAILURE$
5+
^\[main.pointer_primitives.\d+\] line 8 pointer invalid in R_OK\(p, \(unsigned (long (long )?)?int\)1\): FAILURE$
6+
^\[main.pointer_primitives.\d+\] line 8 pointer outside object bounds in R_OK\(p, \(unsigned (long (long )?)?int\)1\): FAILURE$
137
^VERIFICATION FAILED$
148
^EXIT=10$
159
^SIGNAL=0$
1610
--
17-
^\[main.pointer_primitives.\d+\] line 17
11+
^\[main.pointer_primitives.\d+\] line 14
1812
--

‎regression/cbmc/pragma_cprover_enable_all/main.c

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -34,10 +34,10 @@ int main()
3434
float x;
3535
float y;
3636
ABC e;
37-
bool same;
37+
bool readable;
3838
char i;
3939
signed int j;
40-
same = __CPROVER_same_object(p, q);
40+
readable = __CPROVER_r_ok(q, 1);
4141
q = p + 2000000000000;
4242
q = r;
4343
if(nondet_bool())
@@ -71,10 +71,10 @@ int main()
7171
float x;
7272
float y;
7373
ABC e;
74-
bool same;
74+
bool readable;
7575
char i;
7676
signed int j;
77-
same = __CPROVER_same_object(p, q);
77+
readable = __CPROVER_r_ok(q, 1);
7878
q = p + 2000000000000;
7979
q = r;
8080
if(nondet_bool())

‎regression/cbmc/pragma_cprover_enable_all/test.desc

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
CORE broken-smt-backend
22
main.c
33
--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
4-
^\[main\.pointer_primitives\.\d+\] line 77 pointer invalid in POINTER_OBJECT\(\(const void \*\)q\): FAILURE
5-
^\[main\.pointer_primitives\.\d+\] line 77 pointer outside object bounds in POINTER_OBJECT\(\(const void \*\)q\): FAILURE
4+
^\[main\.pointer_primitives\.\d+\] line 77 pointer invalid in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$
5+
^\[main\.pointer_primitives\.\d+\] line 77 pointer outside object bounds in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$
66
^\[main\.pointer_arithmetic\.\d+\] line 78 pointer arithmetic: pointer outside object bounds in p \+ 2000000000000(l|ll): FAILURE
77
^\[main\.NaN\.\d+\] line 84 NaN on / in x / den: FAILURE
88
^\[main\.division-by-zero\.\d+\] line 84 division by zero in x / den: FAILURE
@@ -14,8 +14,8 @@ main.c
1414
^EXIT=10$
1515
^SIGNAL=0$
1616
--
17-
^\[main\.pointer_primitives\.\d+\] line 40 pointer invalid in POINTER_OBJECT\(const void \*\)q\): FAILURE
18-
^\[main\.pointer_primitives\.\d+\] line 40 pointer outside object bounds in POINTER_OBJECT\(const void \*\)q\): FAILURE
17+
^\[main\.pointer_primitives\.\d+\] line 40 pointer invalid in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$
18+
^\[main\.pointer_primitives\.\d+\] line 40 pointer outside object bounds in R_OK\(q, \(unsigned (long (long )?)?int\)1\): FAILURE$
1919
^\[main\.pointer_arithmetic\.\d+\] line 41 pointer arithmetic: pointer outside object bounds in p \+ 2000000000000(l|ll): FAILURE
2020
^\[main\.NaN\.\d+\] line 47 NaN on / in x / den: FAILURE
2121
^\[main\.division-by-zero\.\d+\] line 47 division by zero in x / den: FAILURE
@@ -24,4 +24,4 @@ main.c
2424
^\[main\.overflow\.\d+\] line 49 arithmetic overflow on signed type conversion in \(char\)\(signed int\)i \+ 1\): FAILURE
2525
^\[main\.overflow\.\d+\] line 50 arithmetic overflow on signed \+ in j \+ 1: FAILURE
2626
--
27-
This test uses all possible named-checks to maximize coverage.
27+
This test uses all possible named-checks to maximize coverage.

‎regression/cbmc/pragma_cprover_enable_disable_global_off/main.c

Lines changed: 7 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -1,41 +1,38 @@
1-
#include <stdlib.h>
2-
31
int main()
42
{
5-
char *p = malloc(sizeof(*p));
6-
char *q;
3+
char *p, *q, *r, *s, *t, *v;
74

85
#pragma CPROVER check push
96
#pragma CPROVER check enable "pointer-primitive"
107
// must generate checks
11-
if(__CPROVER_same_object(p, q))
8+
if(__CPROVER_r_ok(p, 1))
129
{
1310
}
1411
#pragma CPROVER check push
1512
#pragma CPROVER check disable "pointer-primitive"
1613
// must not generate checks
17-
if(__CPROVER_same_object(p, q))
14+
if(__CPROVER_r_ok(q, 1))
1815
{
1916
}
2017
#pragma CPROVER check push
2118
#pragma CPROVER check enable "pointer-primitive"
2219
// must generate checks
23-
if(__CPROVER_same_object(p, q))
20+
if(__CPROVER_r_ok(r, 1))
2421
{
2522
}
2623
#pragma CPROVER check pop
2724
// must not generate generate checks
28-
if(__CPROVER_same_object(p, q))
25+
if(__CPROVER_r_ok(s, 1))
2926
{
3027
}
3128
#pragma CPROVER check pop
3229
// must generate generate checks
33-
if(__CPROVER_same_object(p, q))
30+
if(__CPROVER_r_ok(t, 1))
3431
{
3532
}
3633
#pragma CPROVER check pop
3734
// must not generate generate checks
38-
if(__CPROVER_same_object(p, q))
35+
if(__CPROVER_r_ok(v, 1))
3936
{
4037
}
4138
return 0;

0 commit comments

Comments
 (0)