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
|
TypeDecls0.bpl(20,5): Error: more than one declaration of type name: C
TypeDecls0.bpl(13,12): Error: more than one declaration of type variable: a
TypeDecls0.bpl(14,18): Error: more than one declaration of type variable: a
TypeDecls0.bpl(18,17): Error: type variable must occur in map arguments: b
TypeDecls0.bpl(22,9): Error: type constructor received wrong number of arguments: C
TypeDecls0.bpl(24,9): Error: undeclared type: A0
TypeDecls0.bpl(25,9): Error: undeclared type: F
TypeDecls0.bpl(28,9): Error: type constructor received wrong number of arguments: E
TypeDecls0.bpl(30,9): Error: type constructor received wrong number of arguments: E
TypeDecls0.bpl(32,9): Error: type constructor received wrong number of arguments: E
TypeDecls0.bpl(38,11): Error: type constructor received wrong number of arguments: E
TypeDecls0.bpl(38,13): Error: type constructor received wrong number of arguments: E
12 name resolution errors detected in TypeDecls0.bpl
TypeDecls1.bpl(7,13): Error: invalid type for argument 0 in map select: int (expected: <b>[b]a)
TypeDecls1.bpl(13,25): Error: right-hand side in map store with wrong type: int (expected: bool)
TypeDecls1.bpl(19,36): Error: invalid type for argument 0 in map select: <c>[c]c (expected: <b>[b]a)
TypeDecls1.bpl(21,13): Error: invalid type for argument 0 in map select: <a>[<b>[b]a]bool (expected: <b>[b]a)
4 type checking errors detected in TypeDecls1.bpl
Prog0.bpl(17,10): Error: type variable must occur in map arguments: a
Prog0.bpl(29,27): Error: more than one declaration of type variable: beta
Prog0.bpl(32,22): Error: undeclared type: alpha
Prog0.bpl(33,35): Error: undeclared type: alpha
4 name resolution errors detected in Prog0.bpl
Prog1.bpl(18,11): Error: invalid type for argument 0 in map select: int (expected: ref)
Prog1.bpl(19,14): Error: invalid type for argument 1 in map select: int (expected: Field a)
Prog1.bpl(20,17): Error: invalid argument types (bool and int) to binary operator >=
3 type checking errors detected in Prog1.bpl
Prog2.bpl(6,14): Error: trigger does not mention alpha, which does not occur in variables types either
1 type checking errors detected in Prog2.bpl
PolyFuns0.bpl(23,33): Error: invalid type for argument 1 in application of fieldValue: ref (expected: Field a)
PolyFuns0.bpl(40,18): Error: invalid type for argument 1 in application of lessThan: bool (expected: a)
PolyFuns0.bpl(41,43): Error: invalid type for argument 1 in application of lessThan: b (expected: a)
PolyFuns0.bpl(53,55): Error: invalid argument types (<c>[Field c]a and <d>[Field d]d) to binary operator ==
4 type checking errors detected in PolyFuns0.bpl
PolyFuns1.bpl(10,9): Error: invalid type for argument 0 in application of F: <c>[c]c (expected: <b>[b]a)
PolyFuns1.bpl(11,9): Error: invalid type for argument 0 in map select: <c>[c]c (expected: <b>[b]a)
PolyFuns1.bpl(12,31): Error: invalid type for argument 0 in application of F: <c>[c]c (expected: <b>[b]a)
PolyFuns1.bpl(13,31): Error: invalid type for argument 0 in map select: <c>[c]c (expected: <b>[b]a)
PolyFuns1.bpl(17,55): Error: invalid argument types (<c>[Field c]a and <d>[Field d]d) to binary operator ==
PolyFuns1.bpl(18,55): Error: invalid argument types (<c>[Field c]a and <d>[Field d]d) to binary operator ==
PolyFuns1.bpl(28,11): Error: invalid type for argument 0 in call to Uhu: <dd>[Field dd]dd (expected: <c>[Field c]a)
PolyFuns1.bpl(29,15): Error: invalid type for argument 1 in call to Uhu: <cc>[Field cc]T (expected: <d>[Field d]d)
PolyFuns1.bpl(30,12): Error: invalid argument types (<cc>[Field cc]T and <dd>[Field dd]dd) to binary operator ==
PolyFuns1.bpl(31,12): Error: invalid argument types (<dd>[Field dd]dd and <cc>[Field cc]T) to binary operator ==
PolyFuns1.bpl(33,15): Error: invalid type for argument 1 in call to Uhu: <ee>[Field T]ee (expected: <d>[Field d]d)
PolyFuns1.bpl(41,11): Error: invalid argument types (<a>[a,a]int and <b>[b,int]int) to binary operator ==
PolyFuns1.bpl(42,11): Error: invalid argument types (<b>[b,int]int and <c>[int,c]int) to binary operator ==
PolyFuns1.bpl(43,11): Error: invalid argument types (<a>[a,a]int and <c>[int,c]int) to binary operator ==
PolyFuns1.bpl(50,11): Error: invalid argument types (<a,b>[a,a,b]int and <a,b>[a,b,b]int) to binary operator ==
PolyFuns1.bpl(57,54): Error: invalid argument types (Field b and NagainCtor b) to binary operator ==
16 type checking errors detected in PolyFuns1.bpl
PolyProcs0.bpl(11,16): Error: invalid type for argument 0 in map select: Field b (expected: ref)
PolyProcs0.bpl(11,19): Error: invalid type for argument 1 in map select: ref (expected: Field a)
PolyProcs0.bpl(21,30): Error: invalid type for argument 1 in call to FieldAccess: Field int (expected: ref)
PolyProcs0.bpl(21,34): Error: invalid type for argument 2 in call to FieldAccess: ref (expected: Field b)
PolyProcs0.bpl(25,7): Error: invalid type for out-parameter 0 in call to FieldAccess: bool (expected: int)
PolyProcs0.bpl(26,35): Error: invalid type for argument 2 in call to FieldAccess: ref (expected: Field b)
PolyProcs0.bpl(41,35): Error: invalid type for argument 1 in call forall to injective: Field int (expected: ref)
7 type checking errors detected in PolyProcs0.bpl
TypeSynonyms0.bpl(9,5): Error: type synonym could not be resolved because of cycles: Cyclic0 (replacing body with "bool" to continue resolving)
TypeSynonyms0.bpl(10,5): Error: type synonym could not be resolved because of cycles: Cyclic1 (replacing body with "bool" to continue resolving)
TypeSynonyms0.bpl(12,5): Error: type synonym could not be resolved because of cycles: AlsoCyclic (replacing body with "bool" to continue resolving)
TypeSynonyms0.bpl(22,10): Error: type constructor received wrong number of arguments: Field
TypeSynonyms0.bpl(23,10): Error: type synonym received wrong number of arguments: Set
TypeSynonyms0.bpl(26,10): Error: type variable must occur in map arguments: a
6 name resolution errors detected in TypeSynonyms0.bpl
TypeSynonyms1.bpl(46,8): Error: invalid type for argument 0 in application of h: <b>[b,b,<b2>[b2,b,int]int]int (expected: nested2)
1 type checking errors detected in TypeSynonyms1.bpl
Boogie program verifier finished with 1 verified, 0 errors
type Set a = [a]bool;
type Field _;
type Heap = <a>[ref,Field a]a;
type notAllParams a b = Field b;
type Cyclic0 = Cyclic1;
type Cyclic1 = Cyclic0;
type AlsoCyclic a = <b>[AlsoCyclic b]int;
type C _ _;
type C2 b a = C a b;
function f(C int bool) returns (int);
const x: C2 bool int;
const y: Field int bool;
const z: Set int bool;
const d: <a,b>[notAllParams a b]int;
type ref;
<console>(10,-1): Error: type synonym could not be resolved because of cycles: Cyclic0 (replacing body with "bool" to continue resolving)
<console>(12,-1): Error: type synonym could not be resolved because of cycles: Cyclic1 (replacing body with "bool" to continue resolving)
<console>(14,-1): Error: type synonym could not be resolved because of cycles: AlsoCyclic (replacing body with "bool" to continue resolving)
<console>(24,8): Error: type constructor received wrong number of arguments: Field
<console>(26,8): Error: type synonym received wrong number of arguments: Set
<console>(28,8): Error: type variable must occur in map arguments: a
6 name resolution errors detected in TypeSynonyms0.bpl
type Set a = [a]bool;
function union<a>(x: Set a, y: Set a) returns (Set a);
axiom (forall<a> x: Set a, y: Set a, z: a :: (x[z] || y[z]) == union(x, y)[z]);
const intSet0: Set int;
axiom (forall x: int :: intSet0[x] == (x == 0 || x == 2 || x == 3));
const intSet1: Set int;
axiom (forall x: int :: intSet1[x] == (x == 0 - 5 || x == 3));
procedure P();
implementation P()
{
assert (forall x: int :: union(intSet0, intSet1)[x] == (x == 0 - 5 || x == 0 || x == 2 || x == 3));
}
type Set a = [a]bool;
function union<a>(x: Set a, y: Set a) returns (Set a);
axiom (forall<a> x: Set a, y: Set a, z: a :: x[z] || y[z] <==> union(x, y)[z]);
const intSet0: Set int;
axiom (forall x: int :: intSet0[x] <==> x == 0 || x == 2 || x == 3);
const intSet1: Set int;
axiom (forall x: int :: intSet1[x] <==> x == 0 - 5 || x == 3);
procedure P();
implementation P()
{
assert (forall x: int :: union(intSet0, intSet1)[x] <==> x == 0 - 5 || x == 0 || x == 2 || x == 3);
}
Boogie program verifier finished with 0 verified, 0 errors
PolyPolyPoly.bpl(12,26): Error: invalid argument types ([]? and <a>[]C a) to binary operator ==
PolyPolyPoly.bpl(15,23): Error: invalid argument types ([]? and <a>[]C a) to binary operator ==
PolyPolyPoly.bpl(21,57): Error: invalid type for argument 1 in map select: b (expected: a)
3 type checking errors detected in PolyPolyPoly.bpl
PolyPolyPoly2.bpl(5,8): Warning: type parameter a is ambiguous, instantiating to int
PolyPolyPoly2.bpl(7,8): Warning: type parameter a is ambiguous, instantiating to <arg0,res>[arg0]res
PolyPolyPoly2.bpl(11,8): Warning: type parameter a is ambiguous, instantiating to bv0
PolyPolyPoly2.bpl(11,15): Warning: type parameter a is ambiguous, instantiating to bv0
PolyPolyPoly2.bpl(11,27): Warning: type parameter a is ambiguous, instantiating to bv17
PolyPolyPoly2.bpl(12,8): Warning: type parameter a is ambiguous, instantiating to bv17
PolyPolyPoly2.bpl(12,15): Warning: type parameter a is ambiguous, instantiating to bv0
PolyPolyPoly2.bpl(22,7): Warning: type parameter a is ambiguous, instantiating to int
PolyPolyPoly2.bpl(31,3): Warning: type parameter a is ambiguous, instantiating to int
PolyPolyPoly2.bpl(32,3): Warning: type parameter a is ambiguous, instantiating to int
Boogie program verifier finished with 0 verified, 0 errors
ProcParamReordering.bpl(13,15): Error: mismatched type of in-parameter in implementation P: y (named b in implementation)
ProcParamReordering.bpl(15,15): Error: mismatched number of type parameters in procedure implementation: P
2 type checking errors detected in ProcParamReordering.bpl
ParallelAssignment.bpl(17,2): Error: mismatched types in assignment command (cannot assign bool to int)
ParallelAssignment.bpl(18,4): Error: invalid type for argument 0 in map assignment: bool (expected: int)
ParallelAssignment.bpl(20,4): Error: command assigns to a global variable that is not in the enclosing method's modifies clause: z
3 type checking errors detected in ParallelAssignment.bpl
ParallelAssignment2.bpl(9,7): Error: number of left-hand sides does not match number of right-hand sides
ParallelAssignment2.bpl(10,9): Error: variable a is assigned more than once in parallel assignment
2 name resolution errors detected in ParallelAssignment2.bpl
Coercions.bpl(11,8): Error: int cannot be coerced to E <a>[a]int
Coercions.bpl(13,8): Error: C cannot be coerced to D
Coercions.bpl(15,9): Error: int cannot be coerced to D
Coercions.bpl(16,9): Error: int cannot be coerced to E int
4 type checking errors detected in Coercions.bpl
Boogie program verifier finished with 0 verified, 0 errors
|
