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
|
ResolutionErrors.dfy(499,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)
ResolutionErrors.dfy(504,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)
ResolutionErrors.dfy(518,23): Error: type of case bodies do not agree (found Tree<_T1,_T0>, previous types Tree<_T0,_T1>)
ResolutionErrors.dfy(530,24): Error: Wrong number of type arguments (0 instead of 2) passed to class/datatype: Tree
ResolutionErrors.dfy(558,23): Error: type variable 'T' in the function call to 'P' could not determined
ResolutionErrors.dfy(565,23): Error: type variable 'T' in the function call to 'P' could not determined
ResolutionErrors.dfy(578,13): Error: 'new' is not allowed in ghost contexts
ResolutionErrors.dfy(579,9): Error: 'new' is not allowed in ghost contexts
ResolutionErrors.dfy(586,14): Error: new allocation not supported in forall statements
ResolutionErrors.dfy(591,11): Error: the body of the enclosing forall statement is not allowed to update heap locations
ResolutionErrors.dfy(591,14): Error: new allocation not allowed in ghost context
ResolutionErrors.dfy(601,23): Error: 'new' is not allowed in ghost contexts
ResolutionErrors.dfy(608,15): Error: 'new' is not allowed in ghost contexts
ResolutionErrors.dfy(608,15): Error: only ghost methods can be called from this context
ResolutionErrors.dfy(608,10): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(617,17): Error: 'new' is not allowed in ghost contexts
ResolutionErrors.dfy(619,20): Error: only ghost methods can be called from this context
ResolutionErrors.dfy(621,8): Error: calls to methods with side-effects are not allowed inside a hint
ResolutionErrors.dfy(639,21): Error: the type of this expression is underspecified, but it cannot be an opaque type.
ResolutionErrors.dfy(639,21): Error: the type of this expression is underspecified, but it cannot be an opaque type.
ResolutionErrors.dfy(676,8): Error: calls to methods with side-effects are not allowed inside a hint
ResolutionErrors.dfy(686,8): Error: only ghost methods can be called from this context
ResolutionErrors.dfy(689,20): Error: 'decreases *' is not allowed on ghost loops
ResolutionErrors.dfy(700,16): 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(700,16): Error: a hint is not allowed to update heap locations
ResolutionErrors.dfy(701,21): Error: a hint is not allowed to update heap locations
ResolutionErrors.dfy(702,8): Error: calls to methods with side-effects are not allowed inside a hint
ResolutionErrors.dfy(705,19): Error: a while statement used inside a hint is not allowed to have a modifies clause
ResolutionErrors.dfy(724,8): Error: only ghost methods can be called from this context
ResolutionErrors.dfy(727,20): Error: 'decreases *' is not allowed on ghost loops
ResolutionErrors.dfy(732,16): 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(732,16): Error: a hint is not allowed to update heap locations
ResolutionErrors.dfy(733,21): Error: a hint is not allowed to update heap locations
ResolutionErrors.dfy(734,8): Error: calls to methods with side-effects are not allowed inside a hint
ResolutionErrors.dfy(737,19): Error: a while statement used inside a hint is not allowed to have a modifies clause
ResolutionErrors.dfy(762,4): Error: calls to methods with side-effects are not allowed inside a statement expression
ResolutionErrors.dfy(763,4): Error: only ghost methods can be called from this context
ResolutionErrors.dfy(764,4): Error: wrong number of method result arguments (got 0, expected 1)
ResolutionErrors.dfy(775,23): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
ResolutionErrors.dfy(785,4): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(796,36): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(805,17): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
ResolutionErrors.dfy(819,6): Error: RHS (of type B) not assignable to LHS (of type object)
ResolutionErrors.dfy(820,6): Error: RHS (of type int) not assignable to LHS (of type object)
ResolutionErrors.dfy(821,6): Error: RHS (of type B) not assignable to LHS (of type object)
ResolutionErrors.dfy(826,6): Error: RHS (of type G) not assignable to LHS (of type object)
ResolutionErrors.dfy(827,6): Error: RHS (of type Dt) not assignable to LHS (of type object)
ResolutionErrors.dfy(828,6): Error: RHS (of type CoDt) not assignable to LHS (of type object)
ResolutionErrors.dfy(890,4): Error: LHS of array assignment must denote an array element (found seq<int>)
ResolutionErrors.dfy(891,4): Error: LHS of array assignment must denote an array element (found seq<int>)
ResolutionErrors.dfy(896,10): Error: LHS of assignment must denote a mutable field
ResolutionErrors.dfy(897,10): Error: LHS of assignment must denote a mutable field
ResolutionErrors.dfy(898,9): Error: cannot assign to a range of array elements (try the 'forall' statement)
ResolutionErrors.dfy(899,9): Error: cannot assign to a range of array elements (try the 'forall' statement)
ResolutionErrors.dfy(900,5): Error: cannot assign to a range of array elements (try the 'forall' statement)
ResolutionErrors.dfy(901,5): Error: cannot assign to a range of array elements (try the 'forall' statement)
ResolutionErrors.dfy(982,11): Error: Wrong number of type arguments (2 instead of 1) passed to class/datatype: array3
ResolutionErrors.dfy(983,11): Error: Wrong number of type arguments (2 instead of 1) passed to class/datatype: C
ResolutionErrors.dfy(994,7): Error: Duplicate name of top-level declaration: BadSyn2
ResolutionErrors.dfy(991,17): Error: Wrong number of type arguments (0 instead of 1) passed to class/datatype: List
ResolutionErrors.dfy(992,17): Error: Undeclared top-level type or type parameter: badName (did you forget to qualify a name?)
ResolutionErrors.dfy(993,22): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)
ResolutionErrors.dfy(1000,7): Error: Cycle among type synonyms: A -> A
ResolutionErrors.dfy(1003,7): Error: Cycle among type synonyms: A -> B -> A
ResolutionErrors.dfy(1007,7): Error: Cycle among type synonyms: A -> B -> A
ResolutionErrors.dfy(1016,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'D' can be constructed
ResolutionErrors.dfy(1019,7): Error: Cycle among type synonyms: A -> B -> A
ResolutionErrors.dfy(1024,7): Error: Cycle among type synonyms: A -> B -> A
ResolutionErrors.dfy(1043,21): Error: unresolved identifier: x
ResolutionErrors.dfy(1050,35): Error: Wrong number of type arguments (2 instead of 1) passed to opaque type: P
ResolutionErrors.dfy(1062,13): Error: Undeclared top-level type or type parameter: BX (did you forget to qualify a name?)
ResolutionErrors.dfy(1072,6): Error: RHS (of type P<int>) not assignable to LHS (of type P<bool>)
ResolutionErrors.dfy(1077,6): Error: RHS (of type P<A>) not assignable to LHS (of type P<B>)
ResolutionErrors.dfy(1082,6): Error: RHS (of type P<A>) not assignable to LHS (of type P<int>)
ResolutionErrors.dfy(1083,6): Error: RHS (of type P<int>) not assignable to LHS (of type P<A>)
ResolutionErrors.dfy(1088,13): Error: arguments must have the same type (got P<int> and P<X>)
ResolutionErrors.dfy(1089,13): Error: arguments must have the same type (got P<bool> and P<X>)
ResolutionErrors.dfy(1090,13): Error: arguments must have the same type (got P<int> and P<bool>)
ResolutionErrors.dfy(429,2): Error: More than one default constructor
ResolutionErrors.dfy(50,13): Error: 'this' is not allowed in a 'static' context
ResolutionErrors.dfy(111,9): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(112,9): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
ResolutionErrors.dfy(116,11): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(117,9): Error: actual out-parameter 0 is required to be a ghost variable
ResolutionErrors.dfy(124,15): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(128,23): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(135,4): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(139,21): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(140,35): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(149,9): Error: only ghost methods can be called from this context
ResolutionErrors.dfy(155,16): Error: 'decreases *' is not allowed on ghost loops
ResolutionErrors.dfy(196,27): Error: ghost-context break statement is not allowed to break out of non-ghost structure
ResolutionErrors.dfy(219,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
ResolutionErrors.dfy(231,12): Error: trying to break out of more loop levels than there are enclosing loops
ResolutionErrors.dfy(235,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
ResolutionErrors.dfy(240,8): Error: return statement is not allowed in this context (because it is guarded by a specification-only expression)
ResolutionErrors.dfy(435,14): Error: when allocating an object of type 'YHWH', one of its constructor methods must be called
ResolutionErrors.dfy(440,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called
ResolutionErrors.dfy(441,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called
ResolutionErrors.dfy(443,9): Error: class Lamb does not have a default constructor
ResolutionErrors.dfy(839,11): Error: a modifies-clause expression must denote an object or a collection of objects (instead got int)
ResolutionErrors.dfy(843,14): Error: in a ghost context, only ghost fields can be mentioned as frame targets (x)
ResolutionErrors.dfy(846,12): Error: in a ghost context, only ghost fields can be mentioned as frame targets (x)
ResolutionErrors.dfy(854,14): Error: in a ghost context, only ghost fields can be mentioned as frame targets (x)
ResolutionErrors.dfy(864,18): Error: in a ghost context, only ghost fields can be mentioned as frame targets (x)
ResolutionErrors.dfy(875,16): Error: in a ghost context, only ghost fields can be mentioned as frame targets (x)
ResolutionErrors.dfy(1031,23): Error: unresolved identifier: x
ResolutionErrors.dfy(1034,20): Error: unresolved identifier: x
ResolutionErrors.dfy(1037,23): Error: unresolved identifier: x
ResolutionErrors.dfy(1039,19): Error: unresolved identifier: x
ResolutionErrors.dfy(1041,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: a field must be selected via an object, not just a class name
ResolutionErrors.dfy(57,7): Error: unresolved identifier: F
ResolutionErrors.dfy(58,14): Error: an instance function must be selected via an object, not just a class name
ResolutionErrors.dfy(58,7): Error: call to instance function requires an instance
ResolutionErrors.dfy(59,7): Error: unresolved identifier: G
ResolutionErrors.dfy(61,7): Error: unresolved identifier: M
ResolutionErrors.dfy(62,7): Error: call to instance method requires an instance
ResolutionErrors.dfy(63,7): Error: unresolved identifier: N
ResolutionErrors.dfy(66,8): Error: non-function expression is called with parameters
ResolutionErrors.dfy(67,14): Error: member z does not exist in class Global
ResolutionErrors.dfy(86,12): Error: the name 'Benny' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.Benny')
ResolutionErrors.dfy(91,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
ResolutionErrors.dfy(92,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
ResolutionErrors.dfy(94,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
ResolutionErrors.dfy(96,12): Error: wrong number of arguments to datatype constructor Abc (found 2, expected 1)
ResolutionErrors.dfy(258,4): Error: label shadows an enclosing label
ResolutionErrors.dfy(263,2): Error: duplicate label
ResolutionErrors.dfy(289,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called
ResolutionErrors.dfy(290,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called
ResolutionErrors.dfy(292,4): Error: a constructor is only allowed to be called when an object is being allocated
ResolutionErrors.dfy(306,16): Error: arguments must have the same type (got int and DTD_List)
ResolutionErrors.dfy(307,16): Error: arguments must have the same type (got DTD_List and int)
ResolutionErrors.dfy(308,25): Error: arguments must have the same type (got bool and int)
ResolutionErrors.dfy(311,18): Error: ghost fields are allowed only in specification contexts
ResolutionErrors.dfy(320,15): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(345,2): Error: incorrect type of method in-parameter 1 (expected GenericClass<int>, got GenericClass<bool>)
ResolutionErrors.dfy(357,18): Error: incorrect type of datatype constructor argument (found GList<_T0>, expected GList<int>)
ResolutionErrors.dfy(365,6): Error: arguments to + must be int or real or a collection type (instead got bool)
ResolutionErrors.dfy(370,6): Error: all lines in a calculation must have the same type (got int after bool)
ResolutionErrors.dfy(373,6): Error: first argument to ==> must be of type bool (instead got int)
ResolutionErrors.dfy(373,6): Error: second argument to ==> must be of type bool (instead got int)
ResolutionErrors.dfy(374,10): Error: first argument to ==> must be of type bool (instead got int)
ResolutionErrors.dfy(374,10): Error: second argument to ==> must be of type bool (instead got int)
ResolutionErrors.dfy(379,10): Error: first argument to ==> must be of type bool (instead got int)
ResolutionErrors.dfy(379,10): Error: second argument to ==> must be of type bool (instead got int)
ResolutionErrors.dfy(384,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(406,6): Error: calls to methods with side-effects are not allowed inside a hint
ResolutionErrors.dfy(408,12): Error: a hint is not allowed to update heap locations
ResolutionErrors.dfy(410,8): Error: a hint is not allowed to update a variable declared outside the hint
ResolutionErrors.dfy(467,7): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(473,12): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(541,7): Error: let-such-that expressions are allowed only in ghost contexts
ResolutionErrors.dfy(543,7): Error: let-such-that expressions are allowed only in ghost contexts
ResolutionErrors.dfy(543,20): Error: ghost variables are allowed only in specification contexts
ResolutionErrors.dfy(545,7): Error: let-such-that expressions are allowed only in ghost contexts
ResolutionErrors.dfy(546,18): Error: unresolved identifier: w
ResolutionErrors.dfy(653,11): Error: lemmas are not allowed to have modifies clauses
ResolutionErrors.dfy(913,9): Error: unresolved identifier: s
ResolutionErrors.dfy(924,32): Error: RHS (of type (int,int,real)) not assignable to LHS (of type (int,real,int))
ResolutionErrors.dfy(925,37): Error: RHS (of type (int,real,int)) not assignable to LHS (of type (int,real,int,real))
ResolutionErrors.dfy(931,9): Error: condition is expected to be of type bool, but is int
ResolutionErrors.dfy(932,16): Error: member 3 does not exist in datatype _tuple#3
ResolutionErrors.dfy(932,26): Error: member x does not exist in datatype _tuple#2
ResolutionErrors.dfy(932,18): Error: arguments must have the same type (got (int,int,int) and (int,int))
ResolutionErrors.dfy(955,15): Error: arguments to / must have the same type (got real and int)
ResolutionErrors.dfy(956,10): Error: second argument to % must be of type int (instead got real)
ResolutionErrors.dfy(960,7): Error: type conversion to real is allowed only from int (got real)
ResolutionErrors.dfy(961,7): Error: type conversion to int is allowed only from real (got int)
ResolutionErrors.dfy(962,7): Error: type conversion to int is allowed only from real (got nat)
ResolutionErrors.dfy(1101,8): Error: new cannot be applied to a trait
175 resolution/type errors detected in ResolutionErrors.dfy
|
