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
|
start
------ Running regression test AssociationList.chalice
Boogie program verifier finished with 12 verified, 0 errors
------ 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 held field of the target of the release statement might not be writable.
128.7: The mu field of the target of the acquire statement might not be above maxlock.
136.7: The mu field of the target of the acquire statement might not be above maxlock.
145.5: The held field of the target of the release statement might not be writable.
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.10: undefined local variable a
33.12: undefined local variable b
33.14: undefined local variable 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.10: undefined local variable v
62.5: call of undeclared member M 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 held field of the target of the unshare statement might not be writable.
84.5: The held field of the target of the unshare statement might not be writable.
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.
15.7: The held field of the target of the release statement might not be writable.
27.7: The held field of the target of the release statement might not be writable.
Boogie program verifier finished with 6 verified, 3 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 GhostConst.chalice
The program did not typecheck.
7.27: undeclared member c in class C
13.10: ghost variable not allowed here
21.10: ghost variable not allowed here
29.10: ghost fields not allowed here
------ 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 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
------ Running regression test Leaks.chalice
6.3: Monitor invariant is not allowed to hold write permission to this.mu
11.3: Monitor invariant can hold permission of other o.mu field only this.mu if this.mu<<o.mu
16.3: Monitor invariant can hold permission of other o.mu field only this.mu if this.mu<<o.mu
29.3: Monitor invariant can hold permission of other o.mu field only this.mu if this.mu<<o.mu
62.3: Monitor invariant is not allowed to hold write permission to this.mu
Boogie program verifier finished with 7 verified, 5 errors
|
