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
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
|
Boogie program verifier finished with 0 verified, 0 errors
Boogie program verifier finished with 0 verified, 0 errors
Triggers0.bpl(14,31): error: the 'nopats' quantifier attribute expects a string-literal parameter
1 parse errors detected in Triggers0.bpl
Triggers1.bpl(7,17): Error: boolean operators are not allowed in triggers
Triggers1.bpl(11,21): Error: boolean operators are not allowed in triggers
Triggers1.bpl(15,9): Error: boolean operators are not allowed in triggers
Triggers1.bpl(19,10): Error: boolean operators are not allowed in triggers
Triggers1.bpl(23,17): Error: boolean operators are not allowed in triggers
Triggers1.bpl(27,17): Error: boolean operators are not allowed in triggers
Triggers1.bpl(32,17): Error: equality is not allowed in triggers
Triggers1.bpl(36,17): Error: arithmetic comparisons are not allowed in triggers
Triggers1.bpl(45,10): Error: quantifiers are not allowed in triggers
Triggers1.bpl(53,7): Error: trigger must mention all quantified variables, but does not mention: x
Triggers1.bpl(61,7): Error: trigger must mention all quantified variables, but does not mention: y
Triggers1.bpl(62,7): Error: trigger must mention all quantified variables, but does not mention: x
Triggers1.bpl(70,9): Error: a matching pattern must be more than just a variable by itself: x
Triggers1.bpl(82,7): Error: trigger must mention all quantified variables, but does not mention: z
Triggers1.bpl(94,16): Error: a matching pattern must be more than just a variable by itself: x
Triggers1.bpl(95,16): Error: a matching pattern must be more than just a variable by itself: g
Triggers1.bpl(105,40): Error: trigger must mention all quantified variables, but does not mention: y
Triggers1.bpl(106,40): Error: trigger must mention all quantified variables, but does not mention: x
Triggers1.bpl(109,57): Error: trigger must mention all quantified variables, but does not mention: z
Triggers1.bpl(110,57): Error: trigger must mention all quantified variables, but does not mention: y
Triggers1.bpl(111,57): Error: trigger must mention all quantified variables, but does not mention: x
Triggers1.bpl(119,33): Error: cannot refer to a global variable in this context: h1
Triggers1.bpl(120,33): Error: cannot refer to a global variable in this context: h0
23 name resolution errors detected in Triggers1.bpl
const x: int;
const y: int;
const z: int;
const r: real;
const s: real;
const t: real;
const P: bool;
const Q: bool;
const R: bool;
axiom x * (y + z) == x + y * z;
axiom x * y + z == (x + y) * z;
axiom x * y * z == x * y * z;
axiom x * y * z * x == x * y * z;
axiom x div y div z == x div (y div z);
axiom x div y div (z div x) == x div y div z;
axiom x + y mod z == y mod z + x;
axiom (x + y) mod z == x mod z + y mod z;
axiom x / y / z == x / (y / z);
axiom x / y / (z / x) == x / y / z;
axiom x / s / z == x / (s / z);
axiom x / s / (z / x) == x / s / z;
axiom r / s / t == r / (s / t);
axiom r / s / (t / r) == r / s / t;
axiom r * s / t == r * s / t;
axiom r / s * t == r / s * t;
axiom (r * s) ** t == r ** t * s ** t;
axiom r ** (s + t) == r ** s * r ** t;
axiom int(real(x)) == x;
axiom r >= 0e0 ==> real(int(r)) <= r;
axiom int(0e0 - 2e-2) == 0;
axiom int(0e0 - 35e0) == -35;
axiom int(27e-1) == 2;
axiom x - y - z == x - (y - z);
axiom x - y - (z - x) == x - y - z;
axiom x + y - z - x + y == 0;
axiom x + y - z - x + y == x + y - (z - (x + y));
axiom P ==> Q ==> R <==> P ==> Q ==> R;
axiom (P ==> Q) ==> R ==> P <==> (P ==> Q) ==> R;
axiom P <==> Q <==> R;
axiom P ==> Q <==> Q ==> R <==> R ==> P;
axiom (P && Q) || (Q && R);
axiom (P || Q) && (Q || R);
axiom P || Q || Q || R;
axiom P && Q && Q && R;
function f(int) : int;
axiom (forall x: int :: {:xname "hello"} {:weight 5} {:ValueFunc f(x + 1)} { f(x + x) } { f(x) * f(x) } {:nopats f(x + x + x) } f(f(x)) < 200);
Boogie program verifier finished with 0 verified, 0 errors
Boogie program verifier finished with 0 verified, 0 errors
Arrays1.bpl(11,11): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: Q
Arrays1.bpl(14,15): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: Q
2 type checking errors detected in Arrays1.bpl
Types0.bpl(6,18): error: expected identifier before ':'
Types0.bpl(6,12): error: expecting an identifier as parameter name
2 parse errors detected in Types0.bpl
Types1.bpl(6,11): Error: undeclared type: x
Types1.bpl(7,11): Error: undeclared type: x
Types1.bpl(7,14): Error: undeclared type: x
3 name resolution errors detected in Types1.bpl
WhereParsing.bpl(14,37): error: where clause not allowed on the 'implementation' copies of formals
WhereParsing.bpl(15,33): error: where clause not allowed on the 'implementation' copies of formals
WhereParsing.bpl(32,38): error: attributes are not allowed on the 'implementation' copies of formals
3 parse errors detected in WhereParsing.bpl
WhereParsing0.bpl(17,38): error: where clause not allowed on bound variables
WhereParsing0.bpl(18,38): error: where clause not allowed on bound variables
2 parse errors detected in WhereParsing0.bpl
WhereParsing1.bpl(14,27): error: ")" expected
1 parse errors detected in WhereParsing1.bpl
WhereParsing2.bpl(1,14): error: ";" expected
1 parse errors detected in WhereParsing2.bpl
WhereResolution.bpl(28,38): Error: undeclared identifier: alpha
WhereResolution.bpl(32,30): Error: old expressions allowed only in two-state contexts
2 name resolution errors detected in WhereResolution.bpl
BadLabels0.bpl(4,2): Error: more than one declaration of block name: X
BadLabels0.bpl(11,4): Error: more than one declaration of block name: Y
2 name resolution errors detected in BadLabels0.bpl
BadLabels1.bpl(4,3): error: Error: goto label 'X' is undefined
BadLabels1.bpl(5,3): error: Error: goto label 'Y' is undefined
BadLabels1.bpl(47,3): error: Error: break statement is not inside a loop
BadLabels1.bpl(49,5): error: Error: break statement is not inside a loop
BadLabels1.bpl(60,5): error: Error: break label 'B' must designate an enclosing statement
BadLabels1.bpl(63,5): error: Error: break label 'A' must designate an enclosing statement
BadLabels1.bpl(64,5): error: Error: break label 'C' must designate an enclosing statement
BadLabels1.bpl(65,8): error: Error: break label 'F' must designate an enclosing statement
8 parse errors detected in BadLabels1.bpl
LineParse.bpl(1,0): error: Malformed (#line num [filename]) pragma: #line
LineParse.bpl(2,0): error: Malformed (#line num [filename]) pragma: #line
LineParse.bpl(1,0): error: Unrecognized pragma: #dontknow what this is No, I don't well, it's an error is what it is
LineParse.bpl(3,0): error: Unrecognized pragma: #define ASSERT(x) {if (!(x)) { crash(); }} // error: A B C . txt(12,0)
LineParse.bpl(6,2): error: EOF expected
5 parse errors detected in LineParse.bpl
LineResolve.bpl(5,1): Error: undeclared identifier: a
LineResolve.bpl(7,2): Error: undeclared identifier: b
LineResolve.bpl(12,0): Error: undeclared identifier: c
LineResolve.bpl(13,10): Error: undeclared identifier: d
LineResolve.bpl(12,0): Error: undeclared identifier: e
LineResolve.bpl(2,0): Error: undeclared identifier: f
LineResolve.bpl(900,0): Error: undeclared identifier: g
Abc.txt(11,3): Error: undeclared identifier: h
Abc.txt(13,0): Error: undeclared identifier: i
Abc.txt(99,0): Error: undeclared identifier: j
c:\Users\leino\Documents\Programs\MyClass.ssc(104,0): Error: undeclared identifier: k
A B C . txt(12,0): Error: undeclared identifier: l
12 name resolution errors detected in LineResolve.bpl
AttributeParsingErr.bpl(1,33): error: only attributes, not triggers, allowed here
AttributeParsingErr.bpl(3,33): error: only attributes, not triggers, allowed here
AttributeParsingErr.bpl(5,52): error: only attributes, not triggers, allowed here
AttributeParsingErr.bpl(7,37): error: only attributes, not triggers, allowed here
AttributeParsingErr.bpl(9,31): error: only attributes, not triggers, allowed here
AttributeParsingErr.bpl(11,29): error: only attributes, not triggers, allowed here
AttributeParsingErr.bpl(13,13): error: only attributes, not triggers, allowed here
AttributeParsingErr.bpl(15,18): error: only attributes, not triggers, allowed here
AttributeParsingErr.bpl(20,26): error: only attributes, not triggers, allowed here
9 parse errors detected in AttributeParsingErr.bpl
type {:sourcefile "test.ssc"} T;
function {:source "test.scc"} f(int) : int;
const {:description "The largest integer value"} unique MAXINT: int;
axiom {:naming "MyFavoriteAxiom"} (forall i: int :: { f(i) } f(i) == i + 1);
var {:description "memory"} $Heap: [ref,name]any;
var {:sort_of_like_a_trigger (forall i: int :: true)} Bla: [ref,name]any;
procedure {:use_impl 1} foo(x: int) returns (n: int);
implementation {:id 1} foo(x: int) returns (n: int)
{
block1:
return;
}
implementation {:id 2} foo(x: int) returns (n: int)
{
block1:
return;
}
type ref;
type any;
type name;
procedure {:myAttribute "h\n\"ello\"", "again", "and\\" a\"gain\"", again} P();
const again: int;
Boogie program verifier finished with 0 verified, 0 errors
AttributeResolution.bpl(1,18): Error: undeclared identifier: foo
AttributeResolution.bpl(3,18): Error: undeclared identifier: bar
AttributeResolution.bpl(7,15): Error: undeclared identifier: qux
AttributeResolution.bpl(7,41): Error: undeclared identifier: ij
AttributeResolution.bpl(13,21): Error: undeclared identifier: bzzt
AttributeResolution.bpl(15,20): Error: undeclared identifier: blt
AttributeResolution.bpl(5,20): Error: undeclared identifier: baz
AttributeResolution.bpl(9,18): Error: undeclared identifier: mux
AttributeResolution.bpl(11,29): Error: undeclared identifier: fux
9 name resolution errors detected in AttributeResolution.bpl
function \true() : bool;
type \procedure;
procedure \old(any: \procedure) returns (\var: \procedure);
implementation \old(any: \procedure) returns (\var: \procedure)
{
var \modifies: \procedure;
\modifies := any;
\var := \modifies;
}
procedure qux(a: \procedure);
implementation qux(a: \procedure)
{
var \var: \procedure;
var x: bool;
call \var := \old(a);
x := \true();
}
Boogie program verifier finished with 0 verified, 0 errors
Boogie program verifier finished with 0 verified, 0 errors
MapsResolutionErrors.bpl(6,9): Error: type variable must occur in map arguments: b
MapsResolutionErrors.bpl(20,10): Error: type variable must occur in procedure arguments: a
2 name resolution errors detected in MapsResolutionErrors.bpl
Orderings.bpl(12,20): Error: undeclared identifier: x
Orderings.bpl(15,23): Error: c0 occurs more than once as parent
Orderings.bpl(16,19): Error: constant cannot be its own parent
Orderings.bpl(18,20): Error: the parent of a constant has to be a constant
4 name resolution errors detected in Orderings.bpl
BadQuantifier.bpl(3,15): error: invalid QuantifierBody
1 parse errors detected in BadQuantifier.bpl
Boogie program verifier finished with 0 verified, 0 errors
----- SeparateVerification0.bpl
SeparateVerification0.bpl(13,6): Error: undeclared identifier: y
1 name resolution errors detected in SeparateVerification0.bpl
----- SeparateVerification1.bpl SeparateVerification0.bpl
SeparateVerification1.bpl(4,6): Error: undeclared identifier: x
SeparateVerification0.bpl(10,6): Error: undeclared identifier: x
2 name resolution errors detected in SeparateVerification0.bpl
----- SeparateVerification0.bpl SeparateVerification0.bpl
Boogie program verifier finished with 0 verified, 0 errors
----- SeparateVerification0.bpl SeparateVerification0.bpl SeparateVerification1.bpl
Boogie program verifier finished with 0 verified, 0 errors
|