blob: 53443a49c887424afbc4f8bc422d9e815e4c0611 (
plain)
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
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
|
class Cell {
var x: int;
// dispose a read permission to x
method dispose_rd()
requires rd(x);
ensures true;
{
}
// return read permission
method void()
requires rd(x);
ensures rd(x);
{
}
// multiple calls to method that destroys rd(x)
method a1()
requires rd(x);
ensures true;
{
call dispose_rd();
call dispose_rd();
}
// call to method that destroys rd(x) really removes permission
method a2()
requires rd(x);
ensures rd(x);
{
call dispose_rd();
// ERROR: should fail to verify postcondition
}
// forking and method calls of dispose_rd
method a3()
requires rd(x);
ensures true;
{
fork dispose_rd();
call dispose_rd();
fork dispose_rd();
call dispose_rd();
}
// forking and method calls of dispose_rd
method a4()
requires rd(x);
ensures rd(x);
{
fork dispose_rd();
// ERROR: should fail to verify postcondition
}
// forking and method calls of dispose_rd
method a5()
requires rd(x);
ensures rd(x,1);
{
fork dispose_rd();
// OK: giving away an epsilon permission however should work
}
// forking and method calls of dispose_rd
method a6()
requires rd(x);
ensures rd*(x);
{
fork dispose_rd();
// OK: giving away a 'undefined' read permission however should work
}
// multiple forks of dispose_rd
method a7()
requires rd(x);
ensures true;
{
fork dispose_rd();
fork dispose_rd();
fork dispose_rd();
fork dispose_rd();
fork dispose_rd();
fork dispose_rd();
}
// joining to regain permission
method a8(a: int)
requires rd(x);
ensures rd(x)
{
fork tk := void();
join tk;
}
// joining to regain permission
method a9(a: int)
requires rd(x);
ensures rd(x)
{
fork tk := dispose_rd();
join tk;
// ERROR: should fail to verify postcondition
}
// joining to regain permission
method a10(a: int)
requires rd(x);
ensures a == 3 ==> rd(x)
{
fork tk := void();
if (3 == a) {
join tk;
}
}
// finite loop of method calls, preserving rd(x)
method a11()
requires rd(x);
ensures rd(x);
{
var i: int;
i := 0;
while (i < 1000)
invariant rd(x);
{
call void();
i := i+1;
}
}
// forking dispose_rd in a loop (using rd(x,*) to denote unknown read permission)
method a12(a: int)
requires rd(x);
ensures rd*(x);
{
var i: int;
i := 0;
while (i < a)
invariant rd*(x);
{
fork dispose_rd();
i := i+1;
}
}
// forking dispose_rd in a loop (using rd(x,*) to denote unknown read permission)
method a13(a: int)
requires rd(x);
ensures rd(x);
{
var i: int;
i := 0;
while (i < a)
invariant rd*(x);
{
fork dispose_rd();
i := i+1;
}
// ERROR: should fail to verify postcondition
}
// calling dispose_rd in a loop (using rd(x,*) to denote unknown read permission)
method a14()
requires rd(x);
ensures true;
{
call dispose_rd();
var i: int;
i := 0;
while (i < 1000)
invariant rd*(x);
{
call dispose_rd();
i := i+1;
}
}
// return unknown permission
method a15()
requires rd(x);
ensures rd*(x);
{
call dispose_rd();
}
// rd in loop invariant
method a16()
requires rd(x);
ensures rd*(x);
{
call dispose_rd();
var i: int;
i := 0;
while (i < 1000)
invariant acc(x,rd);
{
call void();
i := i+1;
}
}
// rd in method contracts
method a17()
requires acc(x,rd);
{
call dispose_rd();
call a17();
}
// multiple rd in method contracts
method a18()
requires rd(x);
ensures rd(x)
{
call a18a()
call a18b()
}
method a18a()
requires acc(x,2*rd);
ensures acc(x,rd+rd);
{
}
method a18b()
requires acc(x,rd+rd);
ensures acc(x,rd*2);
{
}
}
|
