1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
|
// function_check_mem_01
// This test checks the use of pointer-related predicates in assumptions and
// requires.
// This test currently fails because of the lack of support for assuming
// pointer predicates.
#include <stddef.h>
#define __CPROVER_VALID_MEM(ptr, size) \
__CPROVER_POINTER_OBJECT((ptr)) != __CPROVER_POINTER_OBJECT(NULL) && \
!__CPROVER_invalid_pointer((ptr)) && \
__CPROVER_POINTER_OBJECT((ptr)) != \
__CPROVER_POINTER_OBJECT(__CPROVER_deallocated) && \
__CPROVER_POINTER_OBJECT((ptr)) != \
__CPROVER_POINTER_OBJECT(__CPROVER_dead_object) && \
(__builtin_object_size((ptr), 1) >= (size) && \
__CPROVER_POINTER_OFFSET((ptr)) >= 0l || \
__CPROVER_DYNAMIC_OBJECT((ptr))) && \
(__CPROVER_POINTER_OFFSET((ptr)) >= 0 && \
__CPROVER_malloc_size >= (size) + __CPROVER_POINTER_OFFSET((ptr)) || \
__CPROVER_POINTER_OBJECT((ptr)) != \
__CPROVER_POINTER_OBJECT(__CPROVER_malloc_object))
typedef struct bar
{
int x;
int y;
int z;
} bar;
void foo(bar *x)
__CPROVER_requires(__CPROVER_VALID_MEM(x, sizeof(bar)))
{
x->x += 1;
return
}
int main()
{
bar *y;
__CPROVER_assume(__CPROVER_VALID_MEM(y, sizeof(bar)));
y->x = 0;
return 0;
}
|
