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
|
int G;
int main (int u) {
int *p;
L: p = &G; char *c = &G;
switch (u) {
case 0:
//@ assert \valid(p);
break;
case 1:
//@ assert \valid(p+1);
break;
case 2:
//@ assert \valid((char*)p+1);
break;
case 3:
//@ assert \valid(c+1);
break;
case 4:
//@ assert \valid(c+3);
break;
case 5:
//@ assert \valid(c+4);
break;
case 6:
//@ assert (char *)p < c;
break;
case 7:
//@ assert p <= (int*)1;
break;
case 8:
//@ assert (int)p == 3;
break;
case 9:
//@ assert (int)p != 3;
break;
case 10:
//@ assert \exists int x ; x != 0 ==> *p == x;
break;
case 11:
//@ assert \forall int x ; \true;
break;
case 12:
//@ assert \valid((long long *)5);
break;
case 13:
//@ assert \valid(p);
break;
case 14:
//@ assert (\valid((char*)5));
break;
case 15:
//@ assert p != \null;
break;
case 16:
//@ assert \valid{L}(p);
//@ assert !\at(\valid(p), L);
break;
case 17: {
int x;
p = &x;
//@ assert !\valid{L}(p); // Incorrect
break;
}
}
return 0;
}
|
