Language change: All functions and methods declared lexically outside any class are now

automatically static, and fields are no longer allowed to be declared there.  Stated
differently, all heap state must now be declared inside an explicitly declared class,
and functions and methods declared outside any class can be viewed as belonging to
the module.  The motivating benefit of this change is to no longer need the 'static'
keyword when declaring a module of functions and methods.

1 files changed, 169 insertions, 169 deletions

diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect
index 9ba6a1b3..55a4b1e6 100644
--- a/Test/dafny0/ResolutionErrors.dfy.expect
+++ b/Test/dafny0/ResolutionErrors.dfy.expect
@@ -1,125 +1,133 @@
-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,25): Error: the type of this variable is underspecified

-ResolutionErrors.dfy(558,23): Error: type variable 'T' in the function call to 'P' could not be determined

-ResolutionErrors.dfy(565,25): Error: the type of this variable is underspecified

-ResolutionErrors.dfy(565,23): Error: type variable 'T' in the function call to 'P' could not be 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,29): Error: only ghost methods can be called from this context

-ResolutionErrors.dfy(621,17): Error: calls to methods with side-effects are not allowed inside a hint

-ResolutionErrors.dfy(639,21): Error: the type of this variable is underspecified

-ResolutionErrors.dfy(676,18): Error: calls to methods with side-effects are not allowed inside a hint

-ResolutionErrors.dfy(686,22): 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,18): 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,22): 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,9): 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,17): Error: calls to methods with side-effects are not allowed inside a statement expression

-ResolutionErrors.dfy(763,18): Error: only ghost methods can be called from this context

-ResolutionErrors.dfy(764,18): 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 redirecting types (newtypes, type synonyms): A -> A

-ResolutionErrors.dfy(1003,7): Error: Cycle among redirecting types (newtypes, type synonyms): A -> B -> A

-ResolutionErrors.dfy(1007,7): Error: Cycle among redirecting types (newtypes, 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 redirecting types (newtypes, type synonyms): A -> B -> A

+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 class/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(611,10): Error: ghost variables are allowed only in specification contexts

+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 class/datatype: array3

+ResolutionErrors.dfy(988,11): Error: Wrong number of type arguments (2 instead of 1) passed to class/datatype: 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 class/datatype: List

+ResolutionErrors.dfy(997,17): Error: Undeclared top-level type or type parameter: badName (did you forget to qualify a name?)

+ResolutionErrors.dfy(998,22): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)

+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(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(1113,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(1115,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(1220,26): Error: the type of this variable is underspecified

-ResolutionErrors.dfy(1221,31): Error: the type of this variable is underspecified

-ResolutionErrors.dfy(1222,29): Error: the type of this variable is underspecified

-ResolutionErrors.dfy(1232,34): Error: the type of this variable is underspecified

-ResolutionErrors.dfy(1248,21): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)

-ResolutionErrors.dfy(1249,24): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)

-ResolutionErrors.dfy(1286,16): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (y)

-ResolutionErrors.dfy(1296,18): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)

-ResolutionErrors.dfy(429,2): Error: More than one anonymous constructor

+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?)

+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?)

+ResolutionErrors.dfy(1254,24): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)

+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(432,2): Error: More than one anonymous 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,10): 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,10): 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 anonymous 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 modifies frame targets (x)

-ResolutionErrors.dfy(846,12): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)

-ResolutionErrors.dfy(854,14): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)

-ResolutionErrors.dfy(864,18): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)

-ResolutionErrors.dfy(875,16): Error: in a ghost context, only ghost fields can be mentioned as modifies 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(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 a 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>)

@@ -133,53 +141,45 @@ ResolutionErrors.dfy(62,14): Error: accessing member 'M' requires an instance ex
 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(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,16): Error: wrong number of arguments to datatype constructor David (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,9): Error: a constructor is allowed to be called only 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,5): 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 of a numeric type 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,9): 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,16): 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(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(1101,8): Error: new cannot be applied to a trait

-ResolutionErrors.dfy(1122,13): Error: first argument to / must be of numeric type (instead got set<bool>)

-ResolutionErrors.dfy(1129,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(1144,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating

+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(544,7): Error: let-such-that expressions are allowed only in ghost contexts

+ResolutionErrors.dfy(546,7): Error: let-such-that expressions are allowed only in ghost contexts

+ResolutionErrors.dfy(546,20): Error: ghost variables are allowed only in specification contexts

+ResolutionErrors.dfy(548,7): Error: let-such-that expressions are allowed only in ghost 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

 184 resolution/type errors detected in ResolutionErrors.dfy