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
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
|
start
------ Running regression test cell.chalice
142.5: Assertion might not hold. Insufficient fraction at 142.12 for Cell.valid.
Boogie program verifier finished with 31 verified, 1 error
------ Running regression test counter.chalice
69.5: Monitor invariant might hot hold. The expression at 4.27 might not evaluate to true.
80.5: Assertion might not hold. The expression at 80.12 might not evaluate to true.
119.5: The target of the release statement might not be locked by the current thread.
128.7: The mu field of the target of the acquire statement might not be above waitlevel.
136.7: The mu field of the target of the acquire statement might not be above waitlevel.
145.5: The target of the release statement might not be locked by the current thread.
Boogie program verifier finished with 24 verified, 6 errors
------ Running regression test dining-philosophers.chalice
Boogie program verifier finished with 12 verified, 0 errors
------ Running regression test ForkJoin.chalice
Boogie program verifier finished with 18 verified, 0 errors
------ Running regression test HandOverHand.chalice
Boogie program verifier finished with 10 verified, 0 errors
------ Running regression test iterator.chalice
Boogie program verifier finished with 22 verified, 0 errors
------ Running regression test iterator2.chalice
Boogie program verifier finished with 21 verified, 0 errors
------ Running regression test producer-consumer.chalice
Boogie program verifier finished with 36 verified, 0 errors
------ Running regression test prog0.chalice
The program did not typecheck.
3.17: undeclared member a in class C
3.37: undeclared member a in class C
3.41: undeclared member a in class C
3.12: assert statement requires a boolean expression (found int)
4.5: undeclared member a in class C
4.10: undeclared member a in class C
5.5: undeclared member b in class C
5.10: undeclared member a in class C
5.14: undeclared member b in class C
5.18: undeclared member c in class C
5.26: undeclared member d in class C
6.5: undeclared member b in class C
6.14: undeclared member a in class C
6.18: undeclared member b in class C
6.23: undeclared member c in class C
6.32: undeclared member d in class C
7.5: undeclared member c in class C
7.10: undeclared member a in class C
7.15: undeclared member b in class C
7.20: undeclared member c in class C
7.29: undeclared member d in class C
8.13: undeclared member X in class C
8.19: undeclared member Y in class C
8.13: incorrect type of ==> LHS (expected bool, found int)
8.19: incorrect type of ==> RHS (expected bool, found int)
8.26: undeclared member Z in class C
8.26: incorrect type of ==> RHS (expected bool, found int)
8.33: undeclared member A in class C
8.39: undeclared member B in class C
8.45: undeclared member C in class C
8.39: incorrect type of ==> LHS (expected bool, found int)
8.45: incorrect type of ==> RHS (expected bool, found int)
8.33: incorrect type of ==> LHS (expected bool, found int)
9.12: undeclared member A in class C
9.17: undeclared member B in class C
9.12: incorrect type of && LHS (expected bool, found int)
9.17: incorrect type of && RHS (expected bool, found int)
9.23: undeclared member C in class C
9.28: undeclared member D in class C
9.23: incorrect type of || LHS (expected bool, found int)
9.28: incorrect type of || RHS (expected bool, found int)
9.33: undeclared member E in class C
9.33: incorrect type of || RHS (expected bool, found int)
9.39: undeclared member F in class C
9.39: incorrect type of && RHS (expected bool, found int)
11.21: undeclared member f in class int
11.21: undeclared member g in class int
11.21: undeclared member h in class int
<undefined position>: not-expression requires boolean operand
<undefined position>: incorrect type of + RHS (expected int, found bool)
11.33: not-expression requires boolean operand
11.33: undeclared member f in class bool
11.43: undeclared member f in class int
11.42: not-expression requires boolean operand
11.42: incorrect type of + RHS (expected int, found bool)
13.5: type mismatch in assignment, lhs=int rhs=D
14.5: undeclared member o in class C
14.5: undeclared member f in class int
15.6: undeclared member a in class C
15.10: undeclared member b in class C
15.5: undeclared member y in class int
15.18: undefined class or channel T used in new expression
16.19: undeclared member O in class C
16.14: == requires operands of the same type, found int and bool
16.31: undeclared member O in class C
16.13: != requires operands of the same type, found bool and int
16.13: object in reorder statement must be of a reference type (found bool)
16.41: undeclared member a in class C
16.41: install bound must be of a reference type or Mu type (found int)
16.43: undeclared member b in class C
16.43: install bound must be of a reference type or Mu type (found int)
16.45: undeclared member c in class C
16.45: install bound must be of a reference type or Mu type (found int)
16.51: install bound must be of a reference type or Mu type (found int)
16.53: install bound must be of a reference type or Mu type (found int)
17.13: undeclared member X in class C
17.19: undeclared member Y in class C
17.13: incorrect type of ==> LHS (expected bool, found int)
17.19: incorrect type of ==> RHS (expected bool, found int)
17.13: object in reorder statement must be of a reference type (found bool)
17.27: install bound must be of a reference type or Mu type (found int)
18.13: undeclared member o in class C
18.13: undeclared member f in class int
18.13: object in reorder statement must be of a reference type (found int)
19.11: undeclared member o in class C
19.11: object in share statement must be of a reference type (found int)
20.13: undeclared member o in class C
20.13: object in unshare statement must be of a reference type (found int)
21.13: undeclared member o in class C
21.13: object in acquire statement must be of a reference type (found int)
22.13: undeclared member o in class C
22.13: object in release statement must be of a reference type (found int)
23.16: undeclared member o in class C
23.16: object in rd acquire statement must be of a reference type (found int)
24.16: undeclared member o in class C
24.16: object in rd release statement must be of a reference type (found int)
25.15: undeclared member o in class C
25.15: object in downgrade statement must be of a reference type (found int)
27.17: undeclared member o in class C
27.5: call of undeclared member m in class int
27.10: wrong token type
29.12: rd expression is allowed only in positive predicate contexts
29.15: undeclared member x in class C
29.20: acc expression is allowed only in positive predicate contexts
29.24: undeclared member y in class C
29.12: incorrect type of + LHS (expected int, found bool)
29.20: incorrect type of + RHS (expected int, found bool)
29.29: acc expression is allowed only in positive predicate contexts
29.33: undeclared member z in class C
29.29: incorrect type of + RHS (expected int, found bool)
29.51: undeclared member k in class C
29.57: undeclared member f in class null
29.12: assert statement requires a boolean expression (found int)
30.10: undeclared member f in class C
31.5: wrong number of actual in-parameters in call to C.m (3 instead of 0)
32.5: wrong number of actual in-parameters in call to C.m (3 instead of 0)
33.19: undeclared member o in class C
33.5: call of undeclared member m in class int
34.5: wrong number of actual in-parameters in call to C.m (1 instead of 0)
34.5: wrong number of actual out-parameters in call to C.m (1 instead of 0)
35.13: undeclared member o in class C
35.13: object in reorder statement must be of a reference type (found int)
58.17: undeclared member sqrt2 in class C
58.25: undeclared member sqrt2 in class C
62.17: undeclared member s in class C
62.5: call of undeclared member M in class int
82.5: call of undeclared member MyMethodX in class ImplicitC
83.12: undefined local variable a
83.16: undefined local variable b
83.16: undeclared member k in class int
88.13: the type of the formal argument is not assignable to the actual parameter (expected: ImplicitC, found: int)
88.13: duplicate actual out-parameter: a
89.16: undeclared member b in class ImplicitC
89.16: undeclared member k in class int
96.21: undeclared member chX in class ImplicitC
96.5: receive expression (which has type int) does not denote a channel
97.12: undefined local variable a
97.16: undefined local variable b
97.16: undeclared member k in class int
104.16: the type of the formal argument is not assignable to the actual parameter (expected: ImplicitC, found: int)
104.16: duplicate actual out-parameter: a
105.16: undeclared member b in class ImplicitC
105.16: undeclared member k in class int
------ Running regression test prog1.chalice
9.10: Location might not be readable.
25.5: Location might not be writable
33.14: Location might not be readable.
42.5: Monitor invariant might hot hold. The expression at 5.23 might not evaluate to true.
60.5: Location might not be writable
76.5: The target of the unshare statement might not be shared.
84.5: The target of the unshare statement might not be shared.
Boogie program verifier finished with 16 verified, 7 errors
------ Running regression test prog2.chalice
24.5: Assertion might not hold. The expression at 24.12 might not evaluate to true.
31.13: Location might not be readable.
73.5: Const variable can be assigned to only once.
78.5: Assertion might not hold. The expression at 78.12 might not evaluate to true.
Boogie program verifier finished with 24 verified, 4 errors
------ Running regression test prog3.chalice
76.3: The postcondition at 77.13 might not hold. The expression at 77.13 might not evaluate to true.
76.3: Method might lock/unlock more than allowed.
191.5: The precondition at 182.14 might not hold. Insufficient epsilons at 182.14 for ReadSharing.x.
202.3: The postcondition at 204.13 might not hold. Insufficient epsilons at 204.13 for ReadSharing.x.
Boogie program verifier finished with 51 verified, 4 errors
------ Running regression test prog4.chalice
5.5: Assertion might not hold. The expression at 5.12 might not evaluate to true.
17.7: The target of the release statement might not be locked by the current thread.
17.7: Release might fail because the current thread might hold the read lock.
30.7: The target of the release statement might not be locked by the current thread.
30.7: Release might fail because the current thread might hold the read lock.
34.5: The target of the release statement might not be locked by the current thread.
34.5: Release might fail because the current thread might hold the read lock.
Boogie program verifier finished with 6 verified, 7 errors
------ Running regression test ImplicitLocals.chalice
Boogie program verifier finished with 8 verified, 0 errors
------ Running regression test RockBand.chalice
27.3: The postcondition at 29.13 might not hold. Insufficient fraction at 29.13 for RockBand.Valid.
41.10: Location might not be readable.
50.5: Location might not be writable
58.3: The postcondition at 60.13 might not hold. Insufficient fraction at 60.13 for Guitar.Valid.
77.3: The postcondition at 79.13 might not hold. Insufficient fraction at 79.13 for Vocalist.Valid.
96.3: The postcondition at 98.13 might not hold. Insufficient fraction at 98.13 for Organ.Valid.
Boogie program verifier finished with 29 verified, 6 errors
------ Running regression test swap.chalice
Boogie program verifier finished with 5 verified, 0 errors
------ Running regression test OwickiGries.chalice
Boogie program verifier finished with 5 verified, 0 errors
------ Running regression test ProdConsChannel.chalice
47.3: Method body is not allowed to leave any debt.
61.3: Method body is not allowed to leave any debt.
85.20: Location might not be readable.
123.7: Assertion might not hold. The expression at 123.14 might not evaluate to true.
Boogie program verifier finished with 19 verified, 4 errors
------ Running regression test LoopLockChange.chalice
10.5: Method execution before loop might lock/unlock more than allowed by lockchange clause of loop.
35.5: The loop might lock/unlock more than the lockchange clause allows.
65.5: The loop might lock/unlock more than the lockchange clause allows.
Boogie program verifier finished with 14 verified, 3 errors
------ Running regression test PetersonsAlgorithm.chalice
Boogie program verifier finished with 7 verified, 0 errors
------ Running regression test quantifiers.chalice
57.29: The heap of the callee might not be strictly smaller than the heap of the caller.
Boogie program verifier finished with 11 verified, 1 error
------ Running regression test cell-defaults.chalice
96.5: The heap of the callee might not be strictly smaller than the heap of the caller.
102.5: The heap of the callee might not be strictly smaller than the heap of the caller.
131.5: Assertion might not hold. Automatic fold might fail. Insufficient fraction at 42.5 for Cell.x.
Boogie program verifier finished with 29 verified, 3 errors
------ Running regression test RockBand-automagic.chalice
Boogie program verifier finished with 35 verified, 0 errors
|
