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
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
|
#include <assert.h>
#include <stdlib.h>
struct STRUCTNAME
{
int data;
struct STRUCTNAME *next;
};
int main()
{
int x;
int y;
__CPROVER_assume(x > 0);
__CPROVER_assume(y > x);
// This is always != 0, but symex doesn't know that.
// So, we force it to produce a case split on shadow memory access.
int choice = y / x;
__CPROVER_field_decl_local("field1", (_Bool)0);
struct STRUCTNAME a;
a.next = (struct STRUCTNAME *)0;
assert(__CPROVER_get_field(&a, "field1") == 0);
assert(__CPROVER_get_field(&(a.data), "field1") == 0);
assert(__CPROVER_get_field(&(a.next), "field1") == 0);
__CPROVER_set_field(&(a.data), "field1", 1);
__CPROVER_set_field(&(a.next), "field1", 1);
assert(__CPROVER_get_field(&a, "field1") == 1);
assert(__CPROVER_get_field(&(a.data), "field1") == 1);
assert(__CPROVER_get_field(&(a.next), "field1") == 1);
struct STRUCTNAME b;
b.next = (struct STRUCTNAME *)0;
if(choice)
{
a.next = &b;
}
assert(__CPROVER_get_field(&a, "field1") == 1);
assert(__CPROVER_get_field(&(a.data), "field1") == 1);
assert(__CPROVER_get_field(&(a.next), "field1") == 1);
// No warning here.
assert(__CPROVER_get_field(a.next, "field1") == 0);
// No warning here.
__CPROVER_set_field(&((*(a.next)).data), "field1", 1);
// No warning here.
assert(__CPROVER_get_field(a.next, "field1") == 1);
struct STRUCTNAME c;
c.next = (struct STRUCTNAME *)0;
if(choice)
{
b.next = &c;
}
// No warning here.
assert(__CPROVER_get_field((*(a.next)).next, "field1") == 0);
// No warning here.
__CPROVER_set_field(&((*(*(a.next)).next).data), "field1", 1);
// No warning here.
assert(__CPROVER_get_field((*(a.next)).next, "field1") == 1);
}
|
