Changed computation of ghosts until pass 2 of resolution.

Other clean-up in resolution passes, like:
Include everything of type "char" into bounds that are discovered, and likewise for reference types.
Allow more set comprehensions, determining if they are finite based on their argument type.
Changed CalcExpr.SubExpressions to not include computed expressions.

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