Skip to content

Commit 3140a77

Browse files
tautschnigtautschnig
committed
Make CPROVER intrinsics proper prototypes
Forward declarations without arguments are deprecated in C. Polymorphic built-ins now have dummy declarations that are only in effect when running library checks. Our own C front-end will type check them properly and won't rely on forward declarations.
1 parent 0bb7a04 commit 3140a77

File tree

47 files changed

+224
-245
lines changed

Some content is hidden

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

47 files changed

+224
-245
lines changed

‎doc/cprover-manual/api.md

Lines changed: 1 addition & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -191,11 +191,8 @@ option to verify the preconditions of the primitives.
191191
```C
192192
__CPROVER_size_t __CPROVER_OBJECT_SIZE(const void *p);
193193
_Bool __CPROVER_DYNAMIC_OBJECT(const void *p);
194-
void __CPROVER_r_ok(const T *p);
195194
void __CPROVER_r_ok(const void *p, size_t size);
196-
void __CPROVER_w_ok(const T *p);
197195
void __CPROVER_w_ok(const void *p, size_t size);
198-
void __CPROVER_rw_ok(const T *p);
199196
void __CPROVER_rw_ok(const void *p, size_t size);
200197
```
201198

@@ -207,9 +204,7 @@ object.
207204
The function **\_\_CPROVER\_r_ok** returns true if reading the piece of
208205
memory starting at the given pointer with the given size is safe.
209206
**\_\_CPROVER\_w_ok** does the same with writing, and **\_\_CPROVER\_rw_ok**
210-
returns true when it is safe to do both. These predicates can be given an
211-
optional size; when the size argument is not given, the size of the subtype
212-
(which must not be **void**) of the pointer type is used.
207+
returns true when it is safe to do both.
213208

214209
#### \_\_CPROVER\_havoc\_object
215210

‎regression/cbmc/pointer-predicates/at_bounds1.c

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ int main()
99
if(p != NULL && s != __CPROVER_max_malloc_size)
1010
{
1111
char *q = p + s;
12-
__CPROVER_assert(__CPROVER_r_ok(q, 0), "should be valid");
13-
__CPROVER_assert(!__CPROVER_r_ok(q + 1, 0), "should fail");
12+
__CPROVER_assert(__CPROVER_r_ok(q, 0ull), "should be valid");
13+
__CPROVER_assert(!__CPROVER_r_ok(q + 1, 0ull), "should fail");
1414
}
1515
}

‎regression/cbmc/pointer-predicates/at_bounds1.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE broken-smt-backend new-smt-backend
22
at_bounds1.c
33
--pointer-primitive-check --malloc-fail-null
4-
^\[main.pointer_primitives.\d+\] line 13 pointer outside object bounds in R_OK\(q \+ (\(signed (long (long )?)?int\))?1, (\(unsigned (long (long )?)?int\))?0\): FAILURE$
4+
^\[main.pointer_primitives.\d+\] line 13 pointer outside object bounds in R_OK\(\(const void \*\)\(q \+ (\(signed (long (long )?)?int\))?1\), 0ull\): FAILURE$
55
^\*\* 1 of \d+ failed
66
^VERIFICATION FAILED$
77
^EXIT=10$

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -18,10 +18,10 @@ void main()
1818
__CPROVER_OBJECT_SIZE(p4);
1919

2020
char *p5;
21-
__CPROVER_r_ok(p5, 1);
21+
__CPROVER_r_ok(p5, 1ull);
2222

2323
char *p6;
24-
__CPROVER_w_ok(p6, 1);
24+
__CPROVER_w_ok(p6, 1ull);
2525

2626
char *p7;
2727
__CPROVER_DYNAMIC_OBJECT(p7);

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

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -7,14 +7,14 @@ main.c
77
\[main.pointer_primitives.\d+\] line \d+ deallocated dynamic object in __CPROVER_OBJECT_SIZE\(\(const void \*\)p4\): SUCCESS
88
\[main.pointer_primitives.\d+\] line \d+ dead object in __CPROVER_OBJECT_SIZE\(\(const void \*\)p4\): SUCCESS
99
\[main.pointer_primitives.\d+\] line \d+ pointer outside object bounds in __CPROVER_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
10+
\[main.pointer_primitives.\d+\] line \d+ pointer invalid in R_OK\(\(const void \*\)p5, 1ull\): FAILURE
11+
\[main.pointer_primitives.\d+\] line \d+ deallocated dynamic object in R_OK\(\(const void \*\)p5, 1ull\): SUCCESS
12+
\[main.pointer_primitives.\d+\] line \d+ dead object in R_OK\(\(const void \*\)p5, 1ull\): SUCCESS
13+
\[main.pointer_primitives.\d+\] line \d+ pointer outside object bounds in R_OK\(\(const void \*\)p5, 1ull\): FAILURE
14+
\[main.pointer_primitives.\d+\] line \d+ pointer invalid in W_OK\(\(const void \*\)p6, 1ull\): FAILURE
15+
\[main.pointer_primitives.\d+\] line \d+ deallocated dynamic object in W_OK\(\(const void \*\)p6, 1ull\): SUCCESS
16+
\[main.pointer_primitives.\d+\] line \d+ dead object in W_OK\(\(const void \*\)p6, 1ull\): SUCCESS
17+
\[main.pointer_primitives.\d+\] line \d+ pointer outside object bounds in W_OK\(\(const void \*\)p6, 1ull\): FAILURE
1818
\[main.pointer_primitives.\d+\] line \d+ pointer invalid in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): FAILURE
1919
\[main.pointer_primitives.\d+\] line \d+ deallocated dynamic object in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): SUCCESS
2020
\[main.pointer_primitives.\d+\] line \d+ dead object in IS_DYNAMIC_OBJECT\(\(const void \*\)p7\): SUCCESS

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

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -3,10 +3,10 @@ main.c
33
--pointer-primitive-check
44
^EXIT=10$
55
^SIGNAL=0$
6-
\[main.pointer_primitives.1\] line \d+ pointer invalid in R_OK\(p, .*1\): FAILURE
7-
\[main.pointer_primitives.2\] line \d+ deallocated dynamic object in R_OK\(p, .*1\): SUCCESS
8-
\[main.pointer_primitives.3\] line \d+ dead object in R_OK\(p, .*1\): SUCCESS
9-
\[main.pointer_primitives.4\] line \d+ pointer outside object bounds in R_OK\(p, .*1\): FAILURE
6+
\[main.pointer_primitives.1\] line \d+ pointer invalid in R_OK\(\(const void \*\)p, .*1\): FAILURE
7+
\[main.pointer_primitives.2\] line \d+ deallocated dynamic object in R_OK\(\(const void \*\)p, .*1\): SUCCESS
8+
\[main.pointer_primitives.3\] line \d+ dead object in R_OK\(\(const void \*\)p, .*1\): SUCCESS
9+
\[main.pointer_primitives.4\] line \d+ pointer outside object bounds in R_OK\(\(const void \*\)p, .*1\): FAILURE
1010
--
1111
^warning: ignoring
1212
--

‎regression/cbmc/pragma_cprover3/main.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -20,7 +20,7 @@ int main()
2020
}
2121

2222
// generate check and fail on the following statements
23-
if(__CPROVER_r_ok(q, 1))
23+
if(__CPROVER_r_ok(q, 1ull))
2424
{
2525
}
2626
}

‎regression/cbmc/pragma_cprover3/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,8 @@ CORE new-smt-backend
22
main.c
33
--pointer-primitive-check
44
^main.c function main$
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$
5+
^\[main.pointer_primitives.\d+\] line 23 pointer invalid in R_OK\(\(const void \*\)q, 1ull\): FAILURE$
6+
^\[main.pointer_primitives.\d+\] line 23 pointer outside object bounds in R_OK\(\(const void \*\)q, 1ull\): FAILURE$
77
^VERIFICATION FAILED$
88
^EXIT=10$
99
^SIGNAL=0$

‎regression/cbmc/pragma_cprover_enable3/main.c

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,13 +5,13 @@ int main()
55
#pragma CPROVER check push
66
#pragma CPROVER check enable "pointer-primitive"
77
// generate checks for the following statements and fail
8-
if(__CPROVER_r_ok(p, 1))
8+
if(__CPROVER_r_ok(p, 1ull))
99
{
1010
}
1111
#pragma CPROVER check pop
1212

1313
// but do not generate checks on the following statements
14-
if(__CPROVER_r_ok(q, 1))
14+
if(__CPROVER_r_ok(q, 1ull))
1515
{
1616
}
1717
}

‎regression/cbmc/pragma_cprover_enable3/test.desc

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,8 +2,8 @@ CORE new-smt-backend
22
main.c
33

44
^main.c function main$
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$
5+
^\[main.pointer_primitives.\d+\] line 8 pointer invalid in R_OK\(\(const void \*\)p, 1ull\): FAILURE$
6+
^\[main.pointer_primitives.\d+\] line 8 pointer outside object bounds in R_OK\(\(const void \*\)p, 1ull\): FAILURE$
77
^VERIFICATION FAILED$
88
^EXIT=10$
99
^SIGNAL=0$

‎regression/cbmc/pragma_cprover_enable_all/main.c

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -37,7 +37,7 @@ int main()
3737
bool readable;
3838
char i;
3939
signed int j;
40-
readable = __CPROVER_r_ok(q, 1);
40+
readable = __CPROVER_r_ok(q, 1ull);
4141
q = p + 2000000000000;
4242
q = r;
4343
if(nondet_bool())
@@ -74,7 +74,7 @@ int main()
7474
bool readable;
7575
char i;
7676
signed int j;
77-
readable = __CPROVER_r_ok(q, 1);
77+
readable = __CPROVER_r_ok(q, 1ull);
7878
q = p + 2000000000000;
7979
q = r;
8080
if(nondet_bool())

‎regression/cbmc/pragma_cprover_enable_all/test.desc

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
CORE
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 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$
4+
^\[main\.pointer_primitives\.\d+\] line 77 pointer invalid in R_OK\(\(const void \*\)q, 1ull\): FAILURE$
5+
^\[main\.pointer_primitives\.\d+\] line 77 pointer outside object bounds in R_OK\(\(const void \*\)q, 1ull\): 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 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$
17+
^\[main\.pointer_primitives\.\d+\] line 40 pointer invalid in R_OK\(\(const void \*\)q, 1ull\): FAILURE$
18+
^\[main\.pointer_primitives\.\d+\] line 40 pointer outside object bounds in R_OK\(\(const void \*\)q, 1ull\): 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

‎regression/cbmc/pragma_cprover_enable_disable_global_off/main.c

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -5,34 +5,34 @@ int main()
55
#pragma CPROVER check push
66
#pragma CPROVER check enable "pointer-primitive"
77
// must generate checks
8-
if(__CPROVER_r_ok(p, 1))
8+
if(__CPROVER_r_ok(p, 1ull))
99
{
1010
}
1111
#pragma CPROVER check push
1212
#pragma CPROVER check disable "pointer-primitive"
1313
// must not generate checks
14-
if(__CPROVER_r_ok(q, 1))
14+
if(__CPROVER_r_ok(q, 1ull))
1515
{
1616
}
1717
#pragma CPROVER check push
1818
#pragma CPROVER check enable "pointer-primitive"
1919
// must generate checks
20-
if(__CPROVER_r_ok(r, 1))
20+
if(__CPROVER_r_ok(r, 1ull))
2121
{
2222
}
2323
#pragma CPROVER check pop
2424
// must not generate generate checks
25-
if(__CPROVER_r_ok(s, 1))
25+
if(__CPROVER_r_ok(s, 1ull))
2626
{
2727
}
2828
#pragma CPROVER check pop
2929
// must generate generate checks
30-
if(__CPROVER_r_ok(t, 1))
30+
if(__CPROVER_r_ok(t, 1ull))
3131
{
3232
}
3333
#pragma CPROVER check pop
3434
// must not generate generate checks
35-
if(__CPROVER_r_ok(v, 1))
35+
if(__CPROVER_r_ok(v, 1ull))
3636
{
3737
}
3838
return 0;

‎regression/cbmc/pragma_cprover_enable_disable_global_off/test.desc

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -2,12 +2,12 @@ CORE new-smt-backend
22
main.c
33

44
^main.c function main$
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$
7-
^\[main.pointer_primitives.\d+\] line 20 pointer invalid in R_OK\(r, \(unsigned (long (long )?)?int\)1\): FAILURE$
8-
^\[main.pointer_primitives.\d+\] line 20 pointer outside object bounds in R_OK\(r, \(unsigned (long (long )?)?int\)1\): FAILURE$
9-
^\[main.pointer_primitives.\d+\] line 30 pointer invalid in R_OK\(t, \(unsigned (long (long )?)?int\)1\): FAILURE$
10-
^\[main.pointer_primitives.\d+\] line 30 pointer outside object bounds in R_OK\(t, \(unsigned (long (long )?)?int\)1\): FAILURE$
5+
^\[main.pointer_primitives.\d+\] line 8 pointer invalid in R_OK\(\(const void \*\)p, 1ull\): FAILURE$
6+
^\[main.pointer_primitives.\d+\] line 8 pointer outside object bounds in R_OK\(\(const void \*\)p, 1ull\): FAILURE$
7+
^\[main.pointer_primitives.\d+\] line 20 pointer invalid in R_OK\(\(const void \*\)r, 1ull\): FAILURE$
8+
^\[main.pointer_primitives.\d+\] line 20 pointer outside object bounds in R_OK\(\(const void \*\)r, 1ull\): FAILURE$
9+
^\[main.pointer_primitives.\d+\] line 30 pointer invalid in R_OK\(\(const void \*\)t, 1ull\): FAILURE$
10+
^\[main.pointer_primitives.\d+\] line 30 pointer outside object bounds in R_OK\(\(const void \*\)t, 1ull\): FAILURE$
1111
^VERIFICATION FAILED$
1212
^EXIT=10$
1313
^SIGNAL=0$

‎regression/cbmc/pragma_cprover_enable_disable_global_on/main.c

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -5,34 +5,34 @@ int main()
55
#pragma CPROVER check push
66
#pragma CPROVER check enable "pointer-primitive"
77
// must generate checks
8-
if(__CPROVER_r_ok(p, 1))
8+
if(__CPROVER_r_ok(p, 1ull))
99
{
1010
}
1111
#pragma CPROVER check push
1212
#pragma CPROVER check disable "pointer-primitive"
1313
// must not generate checks
14-
if(__CPROVER_r_ok(q, 1))
14+
if(__CPROVER_r_ok(q, 1ull))
1515
{
1616
}
1717
#pragma CPROVER check push
1818
#pragma CPROVER check enable "pointer-primitive"
1919
// must generate checks
20-
if(__CPROVER_r_ok(r, 1))
20+
if(__CPROVER_r_ok(r, 1ull))
2121
{
2222
}
2323
#pragma CPROVER check pop
2424
// must not generate generate checks
25-
if(__CPROVER_r_ok(s, 1))
25+
if(__CPROVER_r_ok(s, 1ull))
2626
{
2727
}
2828
#pragma CPROVER check pop
2929
// must generate generate checks
30-
if(__CPROVER_r_ok(t, 1))
30+
if(__CPROVER_r_ok(t, 1ull))
3131
{
3232
}
3333
#pragma CPROVER check pop
3434
// must generate generate checks
35-
if(__CPROVER_r_ok(v, 1))
35+
if(__CPROVER_r_ok(v, 1ull))
3636
{
3737
}
3838
return 0;

‎regression/cbmc/pragma_cprover_enable_disable_global_on/test.desc

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -2,14 +2,14 @@ CORE new-smt-backend
22
main.c
33
--pointer-primitive-check
44
^main.c function main$
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$
7-
^\[main.pointer_primitives.\d+\] line 20 pointer invalid in R_OK\(r, \(unsigned (long (long )?)?int\)1\): FAILURE$
8-
^\[main.pointer_primitives.\d+\] line 20 pointer outside object bounds in R_OK\(r, \(unsigned (long (long )?)?int\)1\): FAILURE$
9-
^\[main.pointer_primitives.\d+\] line 30 pointer invalid in R_OK\(t, \(unsigned (long (long )?)?int\)1\): FAILURE$
10-
^\[main.pointer_primitives.\d+\] line 30 pointer outside object bounds in R_OK\(t, \(unsigned (long (long )?)?int\)1\): FAILURE$
11-
^\[main.pointer_primitives.\d+\] line 35 pointer invalid in R_OK\(v, \(unsigned (long (long )?)?int\)1\): FAILURE$
12-
^\[main.pointer_primitives.\d+\] line 35 pointer outside object bounds in R_OK\(v, \(unsigned (long (long )?)?int\)1\): FAILURE$
5+
^\[main.pointer_primitives.\d+\] line 8 pointer invalid in R_OK\(\(const void \*\)p, 1ull\): FAILURE$
6+
^\[main.pointer_primitives.\d+\] line 8 pointer outside object bounds in R_OK\(\(const void \*\)p, 1ull\): FAILURE$
7+
^\[main.pointer_primitives.\d+\] line 20 pointer invalid in R_OK\(\(const void \*\)r, 1ull\): FAILURE$
8+
^\[main.pointer_primitives.\d+\] line 20 pointer outside object bounds in R_OK\(\(const void \*\)r, 1ull\): FAILURE$
9+
^\[main.pointer_primitives.\d+\] line 30 pointer invalid in R_OK\(\(const void \*\)t, 1ull\): FAILURE$
10+
^\[main.pointer_primitives.\d+\] line 30 pointer outside object bounds in R_OK\(\(const void \*\)t, 1ull\): FAILURE$
11+
^\[main.pointer_primitives.\d+\] line 35 pointer invalid in R_OK\(\(const void \*\)v, 1ull\): FAILURE$
12+
^\[main.pointer_primitives.\d+\] line 35 pointer outside object bounds in R_OK\(\(const void \*\)v, 1ull\): FAILURE$
1313
^VERIFICATION FAILED$
1414
^EXIT=10$
1515
^SIGNAL=0$

‎regression/cbmc/r_w_ok10/main.c

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

99
// special value of invalid pointer
1010
char *p2 = (size_t)1 << (sizeof(char *) * 8 - 8);
11-
__CPROVER_r_ok(p2, 1);
11+
__CPROVER_r_ok(p2, 1ull);
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_r_ok(p3, 1);
15+
__CPROVER_r_ok(p3, 1ull);
1616

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

2222
// offset out of bounds
2323
char *p5 = malloc(10);
2424
p5 += 10;
25-
_Bool result = __CPROVER_r_ok(p5, 1);
25+
_Bool result = __CPROVER_r_ok(p5, 1ull);
2626
__CPROVER_assert(!result, "should be false");
2727

2828
// dead
@@ -31,11 +31,11 @@ void main()
3131
char c;
3232
p6 = &c;
3333
}
34-
__CPROVER_r_ok(p6, 1);
34+
__CPROVER_r_ok(p6, 1ull);
3535
*p6;
3636

3737
// deallocated
3838
char *p7 = malloc(1);
3939
free(p7);
40-
__CPROVER_r_ok(p7, 1);
40+
__CPROVER_r_ok(p7, 1ull);
4141
}

‎regression/cbmc/r_w_ok10/test.desc

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -3,14 +3,14 @@ main.c
33
--pointer-primitive-check
44
^EXIT=10$
55
^SIGNAL=0$
6-
^\[main.pointer_primitives.\d+\] line 7 pointer invalid in R_OK\(p1, \(unsigned (long (long )?)?int\)1\): FAILURE$
7-
^\[main.pointer_primitives.\d+\] line 7 pointer outside object bounds in R_OK\(p1, \(unsigned (long (long )?)?int\)1\): FAILURE$
8-
^\[main.pointer_primitives.\d+\] line 11 pointer invalid in R_OK\(p2, \(unsigned (long (long )?)?int\)1\): FAILURE$
9-
^\[main.pointer_primitives.\d+\] line 11 pointer outside object bounds in R_OK\(p2, \(unsigned (long (long )?)?int\)1\): FAILURE$
10-
^\[main.pointer_primitives.\d+\] line 15 pointer outside object bounds in R_OK\(p3, \(unsigned (long (long )?)?int\)1\): FAILURE$
11-
^\[main.pointer_primitives.\d+\] line 20 pointer outside object bounds in R_OK\(p4, \(unsigned (long (long )?)?int\)1\): FAILURE$
12-
^\[main.pointer_primitives.\d+\] line 34 dead object in R_OK\(p6, \(unsigned (long (long )?)?int\)1\): FAILURE$
13-
^\[main.pointer_primitives.\d+\] line 40 deallocated dynamic object in R_OK\(p7, \(unsigned (long (long )?)?int\)1\): FAILURE$
6+
^\[main.pointer_primitives.\d+\] line 7 pointer invalid in R_OK\(\(const void \*\)p1, 1ull\): FAILURE$
7+
^\[main.pointer_primitives.\d+\] line 7 pointer outside object bounds in R_OK\(\(const void \*\)p1, 1ull\): FAILURE$
8+
^\[main.pointer_primitives.\d+\] line 11 pointer invalid in R_OK\(\(const void \*\)p2, 1ull\): FAILURE$
9+
^\[main.pointer_primitives.\d+\] line 11 pointer outside object bounds in R_OK\(\(const void \*\)p2, 1ull\): FAILURE$
10+
^\[main.pointer_primitives.\d+\] line 15 pointer outside object bounds in R_OK\(\(const void \*\)p3, 1ull\): FAILURE$
11+
^\[main.pointer_primitives.\d+\] line 20 pointer outside object bounds in R_OK\(\(const void \*\)p4, 1ull\): FAILURE$
12+
^\[main.pointer_primitives.\d+\] line 34 dead object in R_OK\(\(const void \*\)p6, 1ull\): FAILURE$
13+
^\[main.pointer_primitives.\d+\] line 40 deallocated dynamic object in R_OK\(\(const void \*\)p7, 1ull\): FAILURE$
1414
^\*\* 8 of \d+ failed
1515
--
1616
^warning: ignoring

‎regression/cprover/contracts/check_assigns1.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -19,7 +19,7 @@ void my_function2(int parameter)
1919

2020
void my_function3(int *pointer)
2121
// clang-format off
22-
__CPROVER_requires(__CPROVER_w_ok(pointer))
22+
__CPROVER_requires(__CPROVER_w_ok(pointer, sizeof(int)))
2323
__CPROVER_assigns(*pointer) // passes
2424
// clang-format on
2525
{

0 commit comments

Comments
 (0)