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
|
ResolutionErrors.dfy(502,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)
ResolutionErrors.dfy(507,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)
ResolutionErrors.dfy(521,23): Error: type of case bodies do not agree (found Tree<_T1,_T0>, previous types Tree<_T0,_T1>)
ResolutionErrors.dfy(533,24): Error: Wrong number of type arguments (0 instead of 2) passed to datatype: Tree
ResolutionErrors.dfy(561,25): Error: the type of this variable is underspecified
ResolutionErrors.dfy(561,23): Error: type variable 'T' in the function call to 'P' could not be determined
ResolutionErrors.dfy(568,25): Error: the type of this variable is underspecified
ResolutionErrors.dfy(568,23): Error: type variable 'T' in the function call to 'P' could not be determined
ResolutionErrors.dfy(581,13): Error: 'new' is not allowed in ghost contexts
ResolutionErrors.dfy(582,9): Error: 'new' is not allowed in ghost contexts
ResolutionErrors.dfy(589,14): Error: new allocation not supported in forall statements
ResolutionErrors.dfy(594,11): Error: the body of the enclosing forall statement is not allowed to update heap locations
ResolutionErrors.dfy(594,14): Error: new allocation not allowed in ghost context
ResolutionErrors.dfy(604,23): Error: 'new' is not allowed in ghost contexts
ResolutionErrors.dfy(611,15): Error: 'new' is not allowed in ghost contexts
ResolutionErrors.dfy(611,15): Error: only ghost methods can be called from this context
ResolutionErrors.dfy(620,17): Error: 'new' is not allowed in ghost contexts
ResolutionErrors.dfy(622,29): Error: only ghost methods can be called from this context
ResolutionErrors.dfy(624,17): Error: calls to methods with side-effects are not allowed inside a hint
ResolutionErrors.dfy(642,21): Error: the type of this variable is underspecified
ResolutionErrors.dfy(680,13): Error: calls to methods with side-effects are not allowed inside a hint
ResolutionErrors.dfy(690,17): Error: only ghost methods can be called from this context
ResolutionErrors.dfy(693,15): Error: 'decreases *' is not allowed on ghost loops
ResolutionErrors.dfy(704,11): Error: Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
ResolutionErrors.dfy(704,11): Error: a hint is not allowed to update heap locations
ResolutionErrors.dfy(705,16): Error: a hint is not allowed to update heap locations
ResolutionErrors.dfy(706,13): Error: calls to methods with side-effects are not allowed inside a hint
ResolutionErrors.dfy(709,14): Error: a while statement used inside a hint is not allowed to have a modifies clause
ResolutionErrors.dfy(728,17): Error: only ghost methods can be called from this context
ResolutionErrors.dfy(731,15): Error: 'decreases *' is not allowed on ghost loops
ResolutionErrors.dfy(736,11): Error: Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
ResolutionErrors.dfy(736,11): Error: a hint is not allowed to update heap locations
ResolutionErrors.dfy(737,16): Error: a hint is not allowed to update heap locations
ResolutionErrors.dfy(738,4): Error: calls to methods with side-effects are not allowed inside a hint
ResolutionErrors.dfy(741,14): Error: a while statement used inside a hint is not allowed to have a modifies clause
ResolutionErrors.dfy(766,19): Error: calls to methods with side-effects are not allowed inside a statement expression
ResolutionErrors.dfy(767,20): Error: only ghost methods can be called from this context
ResolutionErrors.dfy(768,20): Error: wrong number of method result arguments (got 0, expected 1)
ResolutionErrors.dfy(780,23): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
ResolutionErrors.dfy(790,4): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(801,36): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(810,17): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
ResolutionErrors.dfy(824,6): Error: RHS (of type B) not assignable to LHS (of type object)
ResolutionErrors.dfy(825,6): Error: RHS (of type int) not assignable to LHS (of type object)
ResolutionErrors.dfy(826,6): Error: RHS (of type B) not assignable to LHS (of type object)
ResolutionErrors.dfy(831,6): Error: RHS (of type G) not assignable to LHS (of type object)
ResolutionErrors.dfy(832,6): Error: RHS (of type Dt) not assignable to LHS (of type object)
ResolutionErrors.dfy(833,6): Error: RHS (of type CoDt) not assignable to LHS (of type object)
ResolutionErrors.dfy(895,4): Error: LHS of array assignment must denote an array element (found seq<int>)
ResolutionErrors.dfy(896,4): Error: LHS of array assignment must denote an array element (found seq<int>)
ResolutionErrors.dfy(901,10): Error: LHS of assignment must denote a mutable field
ResolutionErrors.dfy(902,10): Error: LHS of assignment must denote a mutable field
ResolutionErrors.dfy(903,9): Error: cannot assign to a range of array elements (try the 'forall' statement)
ResolutionErrors.dfy(904,9): Error: cannot assign to a range of array elements (try the 'forall' statement)
ResolutionErrors.dfy(905,5): Error: cannot assign to a range of array elements (try the 'forall' statement)
ResolutionErrors.dfy(906,5): Error: cannot assign to a range of array elements (try the 'forall' statement)
ResolutionErrors.dfy(987,11): Error: Wrong number of type arguments (2 instead of 1) passed to array type: array3
ResolutionErrors.dfy(988,11): Error: Wrong number of type arguments (2 instead of 1) passed to class: C
ResolutionErrors.dfy(999,7): Error: Duplicate name of top-level declaration: BadSyn2
ResolutionErrors.dfy(996,17): Error: Wrong number of type arguments (0 instead of 1) passed to datatype: List
ResolutionErrors.dfy(997,17): Error: Undeclared top-level type or type parameter: badName (did you forget to qualify a name or declare a module import 'opened?')
ResolutionErrors.dfy(998,22): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name or declare a module import 'opened?')
ResolutionErrors.dfy(1005,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> A
ResolutionErrors.dfy(1008,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A
ResolutionErrors.dfy(1012,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A
ResolutionErrors.dfy(1021,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'D' can be constructed
ResolutionErrors.dfy(1024,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A
ResolutionErrors.dfy(1029,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A
ResolutionErrors.dfy(1048,21): Error: unresolved identifier: x
ResolutionErrors.dfy(1055,35): Error: Wrong number of type arguments (2 instead of 1) passed to opaque type: P
ResolutionErrors.dfy(1067,13): Error: Undeclared top-level type or type parameter: BX (did you forget to qualify a name or declare a module import 'opened?')
ResolutionErrors.dfy(1077,6): Error: RHS (of type P<int>) not assignable to LHS (of type P<bool>)
ResolutionErrors.dfy(1082,6): Error: RHS (of type P<A>) not assignable to LHS (of type P<B>)
ResolutionErrors.dfy(1087,6): Error: RHS (of type P<A>) not assignable to LHS (of type P<int>)
ResolutionErrors.dfy(1088,6): Error: RHS (of type P<int>) not assignable to LHS (of type P<A>)
ResolutionErrors.dfy(1093,13): Error: arguments must have the same type (got P<int> and P<X>)
ResolutionErrors.dfy(1094,13): Error: arguments must have the same type (got P<bool> and P<X>)
ResolutionErrors.dfy(1095,13): Error: arguments must have the same type (got P<int> and P<bool>)
ResolutionErrors.dfy(1118,38): Error: a set comprehension must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'o'
ResolutionErrors.dfy(1120,24): Error: a set comprehension must produce a finite set, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'o'
ResolutionErrors.dfy(1225,26): Error: the type of this variable is underspecified
ResolutionErrors.dfy(1226,31): Error: the type of this variable is underspecified
ResolutionErrors.dfy(1227,29): Error: the type of this variable is underspecified
ResolutionErrors.dfy(1237,34): Error: the type of this variable is underspecified
ResolutionErrors.dfy(1253,21): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name or declare a module import 'opened?')
ResolutionErrors.dfy(1254,24): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name or declare a module import 'opened?')
ResolutionErrors.dfy(1291,16): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (y)
ResolutionErrors.dfy(1301,18): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
ResolutionErrors.dfy(1329,15): Error: The name Inner ambiguously refers to a type in one of the modules A, B (try qualifying the type name with the module name)
ResolutionErrors.dfy(1339,29): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(1341,49): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(1341,54): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(1362,11): Error: name of type (X) is used as a variable
ResolutionErrors.dfy(1362,16): Error: name of type (X) is used as a variable
ResolutionErrors.dfy(1363,11): Error: name of module (Y) is used as a variable
ResolutionErrors.dfy(1363,16): Error: name of module (Y) is used as a variable
ResolutionErrors.dfy(1364,11): Error: name of type (X) is used as a variable
ResolutionErrors.dfy(1364,13): Error: second argument to "in" must be a set, multiset, or sequence with elements of type #type, or a map with domain #type (instead got map<real, string>)
ResolutionErrors.dfy(1365,11): Error: name of module (Y) is used as a variable
ResolutionErrors.dfy(1365,13): Error: second argument to "in" must be a set, multiset, or sequence with elements of type #module, or a map with domain #module (instead got map<real, string>)
ResolutionErrors.dfy(1370,16): Error: name of type (X) is used as a variable
ResolutionErrors.dfy(1370,13): Error: arguments must have the same type (got int and #type)
ResolutionErrors.dfy(1371,16): Error: name of module (Y) is used as a variable
ResolutionErrors.dfy(1371,13): Error: arguments must have the same type (got int and #module)
ResolutionErrors.dfy(1372,4): Error: name of type (X) is used as a variable
ResolutionErrors.dfy(1373,4): Error: name of module (Y) is used as a variable
ResolutionErrors.dfy(1382,11): Error: type of RHS of assign-such-that statement must be boolean (got int)
ResolutionErrors.dfy(1383,9): Error: type of RHS of assign-such-that statement must be boolean (got int)
ResolutionErrors.dfy(1384,13): Error: type of RHS of assign-such-that statement must be boolean (got int)
ResolutionErrors.dfy(1387,15): Error: type of RHS of let-such-that expression must be boolean (got int)
ResolutionErrors.dfy(432,2): Error: More than one anonymous constructor
ResolutionErrors.dfy(50,13): Error: 'this' is not allowed in a 'static' context
ResolutionErrors.dfy(87,14): Error: the name 'Benny' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.Benny')
ResolutionErrors.dfy(92,14): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
ResolutionErrors.dfy(93,14): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
ResolutionErrors.dfy(95,14): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
ResolutionErrors.dfy(97,18): Error: wrong number of arguments to datatype constructor David (found 2, expected 1)
ResolutionErrors.dfy(113,9): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(114,9): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
ResolutionErrors.dfy(118,11): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(119,10): Error: actual out-parameter 0 is required to be a ghost variable
ResolutionErrors.dfy(126,15): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(130,23): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(137,4): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(141,21): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(142,35): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(151,10): Error: only ghost methods can be called from this context
ResolutionErrors.dfy(157,16): Error: 'decreases *' is not allowed on ghost loops
ResolutionErrors.dfy(198,27): Error: ghost-context break statement is not allowed to break out of non-ghost structure
ResolutionErrors.dfy(221,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
ResolutionErrors.dfy(233,12): Error: trying to break out of more loop levels than there are enclosing loops
ResolutionErrors.dfy(237,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
ResolutionErrors.dfy(242,8): Error: return statement is not allowed in this context (because it is guarded by a specification-only expression)
ResolutionErrors.dfy(408,11): Error: calls to methods with side-effects are not allowed inside a hint
ResolutionErrors.dfy(410,14): Error: a hint is not allowed to update heap locations
ResolutionErrors.dfy(412,10): Error: a hint is not allowed to update a variable declared outside the hint
ResolutionErrors.dfy(438,14): Error: when allocating an object of type 'YHWH', one of its constructor methods must be called
ResolutionErrors.dfy(443,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called
ResolutionErrors.dfy(444,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called
ResolutionErrors.dfy(446,9): Error: class Lamb does not have an anonymous constructor
ResolutionErrors.dfy(844,11): Error: a modifies-clause expression must denote an object or a collection of objects (instead got int)
ResolutionErrors.dfy(848,14): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
ResolutionErrors.dfy(851,12): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
ResolutionErrors.dfy(859,14): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
ResolutionErrors.dfy(869,18): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
ResolutionErrors.dfy(880,16): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
ResolutionErrors.dfy(1036,23): Error: unresolved identifier: x
ResolutionErrors.dfy(1039,20): Error: unresolved identifier: x
ResolutionErrors.dfy(1042,23): Error: unresolved identifier: x
ResolutionErrors.dfy(1044,19): Error: unresolved identifier: x
ResolutionErrors.dfy(1046,19): Error: unresolved identifier: x
ResolutionErrors.dfy(12,16): Error: 'decreases *' is not allowed on ghost loops
ResolutionErrors.dfy(24,11): Error: array selection requires an array2 (got array3<T>)
ResolutionErrors.dfy(25,12): Error: sequence/array/multiset/map selection requires a sequence, array, multiset, or map (got array3<T>)
ResolutionErrors.dfy(26,11): Error: array selection requires an array4 (got array<T>)
ResolutionErrors.dfy(56,14): Error: accessing member 'X' requires an instance expression
ResolutionErrors.dfy(57,7): Error: unresolved identifier: F
ResolutionErrors.dfy(58,14): Error: accessing member 'F' requires an instance expression
ResolutionErrors.dfy(59,7): Error: unresolved identifier: G
ResolutionErrors.dfy(61,7): Error: unresolved identifier: M
ResolutionErrors.dfy(62,14): Error: accessing member 'M' requires an instance expression
ResolutionErrors.dfy(63,7): Error: unresolved identifier: N
ResolutionErrors.dfy(66,8): Error: non-function expression (of type int) is called with parameters
ResolutionErrors.dfy(67,14): Error: member 'z' does not exist in type 'Global'
ResolutionErrors.dfy(260,4): Error: label shadows an enclosing label
ResolutionErrors.dfy(265,2): Error: duplicate label
ResolutionErrors.dfy(291,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called
ResolutionErrors.dfy(292,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called
ResolutionErrors.dfy(294,9): Error: a constructor is allowed to be called only when an object is being allocated
ResolutionErrors.dfy(308,16): Error: arguments must have the same type (got int and DTD_List)
ResolutionErrors.dfy(309,16): Error: arguments must have the same type (got DTD_List and int)
ResolutionErrors.dfy(310,25): Error: arguments must have the same type (got bool and int)
ResolutionErrors.dfy(313,18): Error: ghost fields are allowed only in specification contexts
ResolutionErrors.dfy(322,15): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(347,5): Error: incorrect type of method in-parameter 1 (expected GenericClass<int>, got GenericClass<bool>)
ResolutionErrors.dfy(359,18): Error: incorrect type of datatype constructor argument (found GList<_T0>, expected GList<int>)
ResolutionErrors.dfy(367,6): Error: arguments to + must be of a numeric type or a collection type (instead got bool)
ResolutionErrors.dfy(372,6): Error: all lines in a calculation must have the same type (got int after bool)
ResolutionErrors.dfy(375,6): Error: first argument to ==> must be of type bool (instead got int)
ResolutionErrors.dfy(375,6): Error: second argument to ==> must be of type bool (instead got int)
ResolutionErrors.dfy(376,10): Error: first argument to ==> must be of type bool (instead got int)
ResolutionErrors.dfy(376,10): Error: second argument to ==> must be of type bool (instead got int)
ResolutionErrors.dfy(381,10): Error: first argument to ==> must be of type bool (instead got int)
ResolutionErrors.dfy(381,10): Error: second argument to ==> must be of type bool (instead got int)
ResolutionErrors.dfy(386,6): Error: print statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
ResolutionErrors.dfy(470,7): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(476,12): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(546,20): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(549,18): Error: unresolved identifier: w
ResolutionErrors.dfy(656,11): Error: lemmas are not allowed to have modifies clauses
ResolutionErrors.dfy(918,9): Error: unresolved identifier: s
ResolutionErrors.dfy(929,32): Error: RHS (of type (int,int,real)) not assignable to LHS (of type (int,real,int))
ResolutionErrors.dfy(930,37): Error: RHS (of type (int,real,int)) not assignable to LHS (of type (int,real,int,real))
ResolutionErrors.dfy(936,16): Error: condition is expected to be of type bool, but is int
ResolutionErrors.dfy(937,16): Error: member 3 does not exist in datatype _tuple#3
ResolutionErrors.dfy(937,26): Error: member x does not exist in datatype _tuple#2
ResolutionErrors.dfy(960,15): Error: arguments to / must have the same type (got real and int)
ResolutionErrors.dfy(961,10): Error: second argument to % must be of type int (instead got real)
ResolutionErrors.dfy(1106,8): Error: new cannot be applied to a trait
ResolutionErrors.dfy(1127,13): Error: first argument to / must be of numeric type (instead got set<bool>)
ResolutionErrors.dfy(1134,18): Error: a call to a possibly non-terminating method is allowed only if the calling method is also declared (with 'decreases *') to be possibly non-terminating
ResolutionErrors.dfy(1149,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating
202 resolution/type errors detected in ResolutionErrors.dfy
|
