Skip to content

Commit 360c01d

Browse files
tautschnigtautschnig
authored
Merge pull request #6491 from tautschnig/pointer-primitive-check-cleanup
Make pointer-primitive-check a no-op when behaviour is always defined
2 parents dbc874e + be35b6c commit 360c01d

File tree

16 files changed

+132
-205
lines changed

16 files changed

+132
-205
lines changed

‎doc/architectural/memory-primitives.md‎

Lines changed: 10 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -199,17 +199,21 @@ CBMC has the option `--pointer-primitive-check` to detect potential misuses of
199199
the memory primitives. It checks that the pointers that appear in the following
200200
primitives are either null or valid:
201201

202-
- `__CPROVER_POINTER_OBJECT`
203-
- `__CPROVER_POINTER_OFFSET`
204-
- `__CPROVER_same_object`
205202
- `__CPROVER_OBJECT_SIZE`
206203
- `__CPROVER_DYNAMIC_OBJECT`
207204
- `__CPROVER_r_ok`
208205
- `__CPROVER_w_ok`
209206

210-
While the first three primitives have well-defined semantics even on invalid
211-
pointers, using them on invalid pointers is usually unintended in user programs.
212-
Thus, they have been included in the `--pointer-primitive-check` option.
207+
The following three primitives have well-defined semantics even on invalid
208+
pointers. Thus, they have been excluded from the `--pointer-primitive-check`
209+
option.
210+
211+
- `__CPROVER_POINTER_OBJECT`
212+
- `__CPROVER_POINTER_OFFSET`
213+
- `__CPROVER_same_object`
214+
215+
Using them on invalid pointers, however, may still be unintended in user
216+
programs.
213217

214218
<sup>1</sup> Pointers with negative offsets never point to memory objects.
215219
Negative values are used internally to detect pointer underflows.

‎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())

0 commit comments

Comments
 (0)