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
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
|
/* run.config*
STDOPT: #" -inout-callwise" +"-print -inout"
*/
volatile int v;
int G;
//@ assigns s[..] \from s[..];
void F1(char *s);
char T[100];
char Tpost[100];
typedef struct {
int f1;
int f2;
} ts;
ts t[10];
int t2[100000];
int t3[100000];
//@ assigns *(p+(0..3)) \from *(p+(4..7));
void f (char *p);
//@ assigns t2[((unsigned char)len)+1 .. ((unsigned char)len)+1] \from \nothing;
void g(int len);
//@ assigns p[..] \from \nothing;
void h(int *p);
/*@ logic int foo(int p) ; */
//@ assigns p[0..foo(*p)] \from \nothing;
void j(int *p);
int x;
int k = 53;
/*@ assigns \at(x, Post) \from \at(x, Post);
assigns Tpost[\at(i, Post)];
assigns Tpost[\at(k, Post)];
*/
void assigns_post(int i);
void main1(void)
{
F1(T);
for (int i=0;i<=5;i++)
f(&t[i].f2);
g(2 * (int)(&T) );
h(2 * (int)(&t3) );
j(T+9);
assigns_post(18);
}
//@ assigns \result;
int ff1();
int* ff2();
//@ assigns \nothing;
int* ff2_bis();
int y1, y2, y3;
/*@ assigns y1, y2, y3; assigns y2 \from y2;*/
void ff3();
void ff4();
int ff5();
int main2() {
int l = ff1();
ff3(); // warn for absence of \from for y1 and y3
ff4(); // No warning, result has type void
ff5(); // No warning, result is unused
int *p = ff2(); // warn on missing assigns \result
int *q = ff2_bis(); // make sure to return NULL in the result
if (p != &x)
return 1;
return 0;
}
int t_main3_1[7][8];
int t_main3_2[3][4][5];
int main3(int a[][8], int b[3][4][5]);
ts t_main4[1000];
ts u_main4[100];
//@ assigns t_main4[i].f1 \from \nothing; assigns u_main4[i].f1 \from \nothing;
void f_main4_1(int i);
//@ assigns t_main4[0..999].f1 \from \nothing; assigns u_main4[0..99].f1 \from \nothing;
void f_main4_2();
void main4() {
f_main4_1(v);
f_main4_2();
}
void main() {
main1();
main2();
main3(t_main3_1, t_main3_2);
main4();
}
|
