1 files changed, 44 insertions, 43 deletions
diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect
index 0286778b..ee2dd5f7 100644
--- a/Test/dafny0/ResolutionErrors.dfy.expect
+++ b/Test/dafny0/ResolutionErrors.dfy.expect
@@ -1,3 +1,21 @@
+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(251,27): Error: ghost-context break statement is not allowed to break out of non-ghost structure
+ResolutionErrors.dfy(274,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
+ResolutionErrors.dfy(288,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
+ResolutionErrors.dfy(293,8): Error: return statement is not allowed in this context (because it is guarded by a specification-only expression)
+ResolutionErrors.dfy(375,15): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(464,11): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(466,14): Error: a hint is not allowed to update heap locations
+ResolutionErrors.dfy(468,10): Error: a hint is not allowed to update a variable declared outside the hint
 ResolutionErrors.dfy(558,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)
 ResolutionErrors.dfy(563,7): Error: RHS (of type List<A>) not assignable to LHS (of type List<B>)
 ResolutionErrors.dfy(577,23): Error: type of case bodies do not agree (found Tree<_T1,_T0>, previous types Tree<_T0,_T1>)
@@ -13,26 +31,11 @@ ResolutionErrors.dfy(652,11): Error: the body of the enclosing forall statement
 ResolutionErrors.dfy(652,14): Error: new allocation not allowed in ghost context
 ResolutionErrors.dfy(662,23): Error: 'new' is not allowed in ghost contexts
 ResolutionErrors.dfy(669,15): Error: 'new' is not allowed in ghost contexts
-ResolutionErrors.dfy(669,15): Error: only ghost methods can be called from this context
 ResolutionErrors.dfy(678,17): Error: 'new' is not allowed in ghost contexts
-ResolutionErrors.dfy(680,29): Error: only ghost methods can be called from this context
-ResolutionErrors.dfy(682,17): Error: calls to methods with side-effects are not allowed inside a hint
 ResolutionErrors.dfy(700,21): Error: the type of this variable is underspecified
-ResolutionErrors.dfy(738,20): Error: calls to methods with side-effects are not allowed inside a hint
-ResolutionErrors.dfy(748,24): Error: only ghost methods can be called from this context
 ResolutionErrors.dfy(751,22): Error: 'decreases *' is not allowed on ghost loops
-ResolutionErrors.dfy(762,18): Error: a hint is not allowed to update heap locations
-ResolutionErrors.dfy(763,23): Error: a hint is not allowed to update heap locations
-ResolutionErrors.dfy(764,20): Error: calls to methods with side-effects are not allowed inside a hint
-ResolutionErrors.dfy(767,21): Error: a while statement used inside a hint is not allowed to have a modifies clause
-ResolutionErrors.dfy(786,24): Error: only ghost methods can be called from this context
 ResolutionErrors.dfy(789,22): Error: 'decreases *' is not allowed on ghost loops
-ResolutionErrors.dfy(794,18): Error: a hint is not allowed to update heap locations
-ResolutionErrors.dfy(795,23): Error: a hint is not allowed to update heap locations
-ResolutionErrors.dfy(796,11): Error: calls to methods with side-effects are not allowed inside a hint
-ResolutionErrors.dfy(799,21): Error: a while statement used inside a hint is not allowed to have a modifies clause
 ResolutionErrors.dfy(824,19): Error: calls to methods with side-effects are not allowed inside a statement expression
-ResolutionErrors.dfy(825,20): Error: only ghost methods can be called from this context
 ResolutionErrors.dfy(826,20): Error: wrong number of method result arguments (got 0, expected 1)
 ResolutionErrors.dfy(838,23): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
 ResolutionErrors.dfy(848,4): Error: ghost variables are allowed only in specification contexts
@@ -74,8 +77,8 @@ ResolutionErrors.dfy(1146,6): Error: RHS (of type P<int>) not assignable to LHS
 ResolutionErrors.dfy(1151,13): Error: arguments must have the same type (got P<int> and P<X>)
 ResolutionErrors.dfy(1152,13): Error: arguments must have the same type (got P<bool> and P<X>)
 ResolutionErrors.dfy(1153,13): Error: arguments must have the same type (got P<int> and P<bool>)
-ResolutionErrors.dfy(1176,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(1178,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(1176,38): Error: set comprehensions in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'o'
+ResolutionErrors.dfy(1178,24): Error: set comprehensions in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce or compile a bounded set of values for 'o'
 ResolutionErrors.dfy(1283,26): Error: the type of this variable is underspecified
 ResolutionErrors.dfy(1284,31): Error: the type of this variable is underspecified
 ResolutionErrors.dfy(1285,29): Error: the type of this variable is underspecified
@@ -106,6 +109,29 @@ ResolutionErrors.dfy(1440,11): Error: type of RHS of assign-such-that statement
 ResolutionErrors.dfy(1441,9): Error: type of RHS of assign-such-that statement must be boolean (got int)
 ResolutionErrors.dfy(1442,13): Error: type of RHS of assign-such-that statement must be boolean (got int)
 ResolutionErrors.dfy(1445,15): Error: type of RHS of let-such-that expression must be boolean (got int)
+ResolutionErrors.dfy(1488,20): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(1510,18): Error: a hint is not allowed to update heap locations
+ResolutionErrors.dfy(1511,23): Error: a hint is not allowed to update heap locations
+ResolutionErrors.dfy(1512,20): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(1515,21): Error: a while statement used inside a hint is not allowed to have a modifies clause
+ResolutionErrors.dfy(1497,24): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(1510,18): 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(1539,18): Error: a hint is not allowed to update heap locations
+ResolutionErrors.dfy(1540,23): Error: a hint is not allowed to update heap locations
+ResolutionErrors.dfy(1541,11): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(1544,21): Error: a while statement used inside a hint is not allowed to have a modifies clause
+ResolutionErrors.dfy(1532,24): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(1539,18): 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(1568,20): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(1461,29): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(1463,17): Error: calls to methods with side-effects are not allowed inside a hint
+ResolutionErrors.dfy(1579,16): Error: 'decreases *' is not allowed on ghost loops
+ResolutionErrors.dfy(1597,12): Error: trying to break out of more loop levels than there are enclosing loops
+ResolutionErrors.dfy(1623,16): Error: ghost fields are allowed only in specification contexts
+ResolutionErrors.dfy(1630,9): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(1636,4): Error: non-ghost variable cannot be assigned a value that depends on a ghost
+ResolutionErrors.dfy(1653,8): 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(1662,26): Error: ghost variables are allowed only in specification contexts
 ResolutionErrors.dfy(488,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')
@@ -113,25 +139,6 @@ ResolutionErrors.dfy(92,14): Error: the name 'David' denotes a datatype construc
 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(231,12): Error: trying to break out of more loop levels than there are enclosing loops
-ResolutionErrors.dfy(251,27): Error: ghost-context break statement is not allowed to break out of non-ghost structure
-ResolutionErrors.dfy(274,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
-ResolutionErrors.dfy(288,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
-ResolutionErrors.dfy(293,8): Error: return statement is not allowed in this context (because it is guarded by a specification-only expression)
-ResolutionErrors.dfy(464,11): Error: calls to methods with side-effects are not allowed inside a hint
-ResolutionErrors.dfy(466,14): Error: a hint is not allowed to update heap locations
-ResolutionErrors.dfy(468,10): Error: a hint is not allowed to update a variable declared outside the hint
 ResolutionErrors.dfy(494,14): Error: when allocating an object of type 'YHWH', one of its constructor methods must be called
 ResolutionErrors.dfy(499,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called
 ResolutionErrors.dfy(500,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called
@@ -168,8 +175,6 @@ ResolutionErrors.dfy(345,9): Error: a constructor is allowed to be called only w
 ResolutionErrors.dfy(359,16): Error: arguments must have the same type (got int and DTD_List)
 ResolutionErrors.dfy(360,16): Error: arguments must have the same type (got DTD_List and int)
 ResolutionErrors.dfy(361,25): Error: arguments must have the same type (got bool and int)
-ResolutionErrors.dfy(367,14): Error: ghost fields are allowed only in specification contexts
-ResolutionErrors.dfy(375,15): Error: ghost variables are allowed only in specification contexts
 ResolutionErrors.dfy(400,5): Error: incorrect type of method in-parameter 1 (expected GenericClass<int>, got GenericClass<bool>)
 ResolutionErrors.dfy(412,18): Error: incorrect type of datatype constructor argument (found GList<_T0>, expected GList<int>)
 ResolutionErrors.dfy(420,6): Error: arguments to + must be of a numeric type or a collection type (instead got bool)
@@ -180,11 +185,7 @@ ResolutionErrors.dfy(429,10): Error: first argument to ==> must be of type bool
 ResolutionErrors.dfy(429,10): Error: second argument to ==> must be of type bool (instead got int)
 ResolutionErrors.dfy(434,10): Error: first argument to ==> must be of type bool (instead got int)
 ResolutionErrors.dfy(434,10): Error: second argument to ==> must be of type bool (instead got int)
-ResolutionErrors.dfy(442,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(526,7): Error: ghost variables are allowed only in specification contexts
-ResolutionErrors.dfy(532,2): Error: non-ghost variable cannot be assigned a value that depends on a ghost
 ResolutionErrors.dfy(603,18): Error: unresolved identifier: w
-ResolutionErrors.dfy(608,24): Error: ghost variables are allowed only in specification contexts
 ResolutionErrors.dfy(714,11): Error: lemmas are not allowed to have modifies clauses
 ResolutionErrors.dfy(976,9): Error: unresolved identifier: s
 ResolutionErrors.dfy(987,32): Error: RHS (of type (int,int,real)) not assignable to LHS (of type (int,real,int))
@@ -198,4 +199,4 @@ ResolutionErrors.dfy(1164,8): Error: new cannot be applied to a trait
 ResolutionErrors.dfy(1185,13): Error: first argument to / must be of numeric type (instead got set<bool>)
 ResolutionErrors.dfy(1192,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(1207,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating
-200 resolution/type errors detected in ResolutionErrors.dfy
+201 resolution/type errors detected in ResolutionErrors.dfy