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.
author: leino <unknown> 2015-09-28 13:16:15 -0700
committer: leino <unknown> 2015-09-28 13:16:15 -0700
commit: 0c1ec594e68dab4fcd458a00f9f7a1ac6de2e218 (patch)
tree: cb89d6ef66c96bfa171f954898548f295a3cabc0
parent: ebaaa36321463925dc9030455e87ae17732b2353 (diff)
18 files changed, 925 insertions, 406 deletions
diff --git a/Binaries/DafnyRuntime.cs b/Binaries/DafnyRuntime.cs
index d1a3c092..4dda19fe 100644
--- a/Binaries/DafnyRuntime.cs
+++ b/Binaries/DafnyRuntime.cs
@@ -1012,6 +1012,12 @@ namespace Dafny
         return pred(false) || pred(true);
       }
     }
+    public static bool QuantChar(bool frall, System.Predicate<char> pred) {
+      for (int i = 0; i < 0x10000; i++) {
+        if (pred((char)i) != frall) { return !frall; }
+      }
+      return frall;
+    }
     public static bool QuantInt(BigInteger lo, BigInteger hi, bool frall, System.Predicate<BigInteger> pred) {
       for (BigInteger i = lo; i < hi; i++) {
         if (pred(i) != frall) { return !frall; }
@@ -1051,6 +1057,13 @@ namespace Dafny
         yield return true;
       }
     }
+    public static IEnumerable<char> AllChars {
+      get {
+        for (int i = 0; i < 0x10000; i++) {
+          yield return (char)i;
+        }
+      }
+    }
     public static IEnumerable<BigInteger> AllIntegers {
       get {
         yield return new BigInteger(0);
diff --git a/Source/Dafny/Cloner.cs b/Source/Dafny/Cloner.cs
index dd2eed69..032e30a0 100644
--- a/Source/Dafny/Cloner.cs
+++ b/Source/Dafny/Cloner.cs
@@ -550,13 +550,21 @@ namespace Microsoft.Dafny
         r = new ForallStmt(Tok(s.Tok), Tok(s.EndTok), s.BoundVars.ConvertAll(CloneBoundVar), null, CloneExpr(s.Range), s.Ens.ConvertAll(CloneMayBeFreeExpr), CloneStmt(s.Body));
 
       } else if (stmt is CalcStmt) {
-          var s = (CalcStmt)stmt;
-          r = new CalcStmt(Tok(s.Tok), Tok(s.EndTok), CloneCalcOp(s.Op), s.Lines.ConvertAll(CloneExpr), s.Hints.ConvertAll(CloneBlockStmt), s.StepOps.ConvertAll(CloneCalcOp), CloneCalcOp(s.ResultOp), CloneAttributes(s.Attributes));
+        var s = (CalcStmt)stmt;
+        // calc statements have the unusual property that the last line is duplicated.  If that is the case (which
+        // we expect it to be here), we share the clone of that line as well.
+        var lineCount = s.Lines.Count;
+        var lines = new List<Expression>(lineCount);
+        for (int i = 0; i < lineCount; i++) {
+          lines.Add(i == lineCount - 1 && 2 <= lineCount && s.Lines[i] == s.Lines[i - 1] ? lines[i - 1] : CloneExpr(s.Lines[i]));
+        }
+        Contract.Assert(lines.Count == lineCount);
+        r = new CalcStmt(Tok(s.Tok), Tok(s.EndTok), CloneCalcOp(s.Op), lines, s.Hints.ConvertAll(CloneBlockStmt), s.StepOps.ConvertAll(CloneCalcOp), CloneCalcOp(s.ResultOp), CloneAttributes(s.Attributes));
 
       } else if (stmt is MatchStmt) {
         var s = (MatchStmt)stmt;
         r = new MatchStmt(Tok(s.Tok), Tok(s.EndTok), CloneExpr(s.Source),
-          s.Cases.ConvertAll(CloneMatchCaseStmt), s.UsesOptionalBraces);
+        s.Cases.ConvertAll(CloneMatchCaseStmt), s.UsesOptionalBraces);
 
       } else if (stmt is AssignSuchThatStmt) {
         var s = (AssignSuchThatStmt)stmt;
diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index 477acabf..cdd968cf 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/Dafny/Compiler.cs
@@ -1566,6 +1566,9 @@ namespace Microsoft.Dafny {
           if (bound is ComprehensionExpr.BoolBoundedPool) {
             Indent(ind);
             wr.Write("foreach (var @{0} in Dafny.Helpers.AllBooleans) {{ ", bv.CompileName);
+          } else if (bound is ComprehensionExpr.CharBoundedPool) {
+            Indent(ind);
+            wr.Write("foreach (var @{0} in Dafny.Helpers.AllChars) {{ ", bv.CompileName);
           } else if (bound is ComprehensionExpr.IntBoundedPool) {
             var b = (ComprehensionExpr.IntBoundedPool)bound;
             Indent(ind);
@@ -1777,6 +1780,8 @@ namespace Microsoft.Dafny {
         Indent(ind);
         if (bound is ComprehensionExpr.BoolBoundedPool) {
           wr.WriteLine("foreach (var {0} in Dafny.Helpers.AllBooleans) {{ @{1} = {0};", tmpVar, bv.CompileName);
+        } else if (bound is ComprehensionExpr.CharBoundedPool) {
+          wr.WriteLine("foreach (var {0} in Dafny.Helpers.AllChars) {{ @{1} = {0};", tmpVar, bv.CompileName);
         } else if (bound is ComprehensionExpr.IntBoundedPool) {
           var b = (ComprehensionExpr.IntBoundedPool)bound;
           if (AsNativeType(bv.Type) != null) {
@@ -2831,6 +2836,8 @@ namespace Microsoft.Dafny {
           // emit:  Dafny.Helpers.QuantX(boundsInformation, isForall, bv => body)
           if (bound is ComprehensionExpr.BoolBoundedPool) {
             wr.Write("Dafny.Helpers.QuantBool(");
+          } else if (bound is ComprehensionExpr.CharBoundedPool) {
+            wr.Write("Dafny.Helpers.QuantChar(");
           } else if (bound is ComprehensionExpr.IntBoundedPool) {
             var b = (ComprehensionExpr.IntBoundedPool)bound;
             wr.Write("Dafny.Helpers.QuantInt(");
@@ -2898,6 +2905,8 @@ namespace Microsoft.Dafny {
           var bv = e.BoundVars[i];
           if (bound is ComprehensionExpr.BoolBoundedPool) {
             wr.Write("foreach (var @{0} in Dafny.Helpers.AllBooleans) {{ ", bv.CompileName);
+          } else if (bound is ComprehensionExpr.CharBoundedPool) {
+            wr.Write("foreach (var @{0} in Dafny.Helpers.AllChars) {{ ", bv.CompileName);
           } else if (bound is ComprehensionExpr.IntBoundedPool) {
             var b = (ComprehensionExpr.IntBoundedPool)bound;
             if (AsNativeType(bv.Type) != null) {
@@ -2971,6 +2980,8 @@ namespace Microsoft.Dafny {
         var bv = e.BoundVars[0];
         if (bound is ComprehensionExpr.BoolBoundedPool) {
           wr.Write("foreach (var @{0} in Dafny.Helpers.AllBooleans) {{ ", bv.CompileName);
+        } else if (bound is ComprehensionExpr.CharBoundedPool) {
+          wr.Write("foreach (var @{0} in Dafny.Helpers.AllChars) {{ ", bv.CompileName);
         } else if (bound is ComprehensionExpr.IntBoundedPool) {
           var b = (ComprehensionExpr.IntBoundedPool)bound;
           if (AsNativeType(bv.Type) != null) {
diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 2a98d5c2..b460d9b4 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -509,6 +509,27 @@ namespace Microsoft.Dafny {
       }
     }
 
+    public bool HasFinitePossibleValues {
+      get {
+        if (IsBoolType || IsCharType || IsRefType) {
+          return true;
+        }
+        var st = AsSetType;
+        if (st != null && st.Arg.HasFinitePossibleValues) {
+          return true;
+        }
+        var mt = AsMapType;
+        if (mt != null && mt.Domain.HasFinitePossibleValues) {
+          return true;
+        }
+        var dt = AsDatatype;
+        if (dt != null && dt.HasFinitePossibleValues) {
+          return true;
+        }
+        return false;
+      }
+    }
+
     public CollectionType AsCollectionType { get { return NormalizeExpand() as CollectionType; } }
     public SetType AsSetType { get { return NormalizeExpand() as SetType; } }
     public MultiSetType AsMultiSetType { get { return NormalizeExpand() as MultiSetType; } }
@@ -2377,6 +2398,48 @@ namespace Microsoft.Dafny {
     }
 
     /// <summary>
+    /// Returns the non-null expressions of this declaration proper (that is, do not include the expressions of substatements).
+    /// Does not include the generated class members.
+    /// </summary>
+    public virtual IEnumerable<Expression> SubExpressions {
+      get {
+        foreach (var e in Attributes.SubExpressions(Attributes)) {
+          yield return e;
+        }
+        foreach (var e in Attributes.SubExpressions(Reads.Attributes)) {
+          yield return e;
+        }
+        foreach (var e in Reads.Expressions) {
+          yield return e.E;
+        }
+        foreach (var e in Attributes.SubExpressions(Modifies.Attributes)) {
+          yield return e;
+        }
+        foreach (var e in Modifies.Expressions) {
+          yield return e.E;
+        }
+        foreach (var e in Attributes.SubExpressions(Decreases.Attributes)) {
+          yield return e;
+        }
+        foreach (var e in Decreases.Expressions) {
+          yield return e;
+        }
+        foreach (var e in Requires) {
+          yield return e.E;
+        }
+        foreach (var e in Ensures) {
+          yield return e.E;
+        }
+        foreach (var e in YieldRequires) {
+          yield return e.E;
+        }
+        foreach (var e in YieldEnsures) {
+          yield return e.E;
+        }
+      }
+    }
+
+    /// <summary>
     /// This Dafny type exists only for the purpose of giving the yield-count variable a type, so
     /// that the type can be recognized during translation of Dafny into Boogie.  It represents
     /// an integer component in a "decreases" clause whose order is (\lambda x,y :: x GREATER y),
@@ -2475,6 +2538,11 @@ namespace Microsoft.Dafny {
         return EnclosingClass.FullCompileName + ".@" + CompileName;
       }
     }
+    public virtual IEnumerable<Expression> SubExpressions {
+      get {
+        yield break;
+      }
+    }
   }
 
   public class Field : MemberDecl {
@@ -2999,6 +3067,26 @@ namespace Microsoft.Dafny {
     public bool IsBuiltin;
     public Function OverriddenFunction;
 
+    public override IEnumerable<Expression> SubExpressions {
+      get {
+        foreach (var e in Req) {
+          yield return e;
+        }
+        foreach (var e in Reads) {
+          yield return e.E;
+        }
+        foreach (var e in Ens) {
+          yield return e;
+        }
+        foreach (var e in Decreases.Expressions) {
+          yield return e;
+        }
+        if (Body != null) {
+          yield return Body;
+        }
+      }
+    }
+
     public Type Type {
       get {
         // Note, the following returned type can contain type parameters from the function and its enclosing class
@@ -3213,6 +3301,24 @@ namespace Microsoft.Dafny {
     public readonly ISet<IVariable> AssignedAssumptionVariables = new HashSet<IVariable>();
     public Method OverriddenMethod;
 
+    public override IEnumerable<Expression> SubExpressions {
+      get {
+        foreach (var e in Req) {
+          yield return e.E;
+        }
+        foreach (var e in Mod.Expressions) {
+          yield return e.E;
+        }
+        foreach (var e in Ens) {
+          yield return e.E;
+        }
+        foreach (var e in Decreases.Expressions) {
+          yield return e;
+        }
+      }
+    }
+
+
     [ContractInvariantMethod]
     void ObjectInvariant() {
       Contract.Invariant(cce.NonNullElements(TypeArgs));
@@ -4821,18 +4927,32 @@ namespace Microsoft.Dafny {
     }
     public override IEnumerable<Expression> SubExpressions
     {
-      get { // FIXME: This can return duplicates; this could confuse BottomUpVisitors that modify the AST in place
+      get {
         foreach (var e in base.SubExpressions) { yield return e; }
         foreach (var e in Attributes.SubExpressions(Attributes)) { yield return e; }
-        
-        foreach (var l in Lines) {
-          yield return l;
+
+        for (int i = 0; i < Lines.Count - 1; i++) {  // note, we skip the duplicated line at the end
+          yield return Lines[i];
         }
-        foreach (var e in Steps) {
-          yield return e;
+        foreach (var calcop in AllCalcOps) {
+          var o3 = calcop as TernaryCalcOp;
+          if (o3 != null) {
+            yield return o3.Index;
+          }
+        }
+      }
+    }
+
+    IEnumerable<CalcOp> AllCalcOps {
+      get {
+        if (Op != null) {
+          yield return Op;
         }
-        if (Result != null) {
-          yield return Result;
+        foreach (var stepop in StepOps) {
+          yield return stepop;
+        }
+        if (ResultOp != null) {
+          yield return ResultOp;
         }
       }
     }
@@ -6637,7 +6757,7 @@ namespace Microsoft.Dafny {
     public readonly Expression Body;
     public readonly bool Exact;  // Exact==true means a regular let expression; Exact==false means an assign-such-that expression
     public readonly Attributes Attributes;
-    public List<ComprehensionExpr.BoundedPool> Constraint_Bounds;  // initialized and filled in by resolver; null for Exact=true and for a ghost statement
+    public List<ComprehensionExpr.BoundedPool> Constraint_Bounds;  // initialized and filled in by resolver; null for Exact=true and for when expression is in a ghost context
     // invariant Constraint_Bounds == null || Constraint_Bounds.Count == BoundVars.Count;
     public List<IVariable> Constraint_MissingBounds;  // filled in during resolution; remains "null" if Exact==true or if bounds can be found
     // invariant Constraint_Bounds == null || Constraint_MissingBounds == null;
@@ -6790,6 +6910,22 @@ namespace Microsoft.Dafny {
         return 5;
       }
     }
+    public class CharBoundedPool : BoundedPool
+    {
+      public override int Preference() {
+        return 4;
+      }
+    }
+    public class RefBoundedPool : BoundedPool
+    {
+      public Type Type;
+      public RefBoundedPool(Type t) {
+        Type = t;
+      }
+      public override int Preference() {
+        return 2;
+      }
+    }
     public class IntBoundedPool : BoundedPool
     {
       public readonly Expression LowerBound;
@@ -6864,6 +7000,24 @@ namespace Microsoft.Dafny {
     public List<BoundVar> MissingBounds;  // filled in during resolution; remains "null" if bounds can be found
     // invariant Bounds == null || MissingBounds == null;
 
+    public List<BoundVar> UncompilableBoundVars() {
+      var bvs = new List<BoundVar>();
+      if (MissingBounds != null) {
+        bvs.AddRange(MissingBounds);
+      }
+      if (Bounds != null) {
+        Contract.Assert(Bounds.Count == BoundVars.Count);
+        for (int i = 0; i < Bounds.Count; i++) {
+          var bound = Bounds[i];
+          if (bound is RefBoundedPool) {
+            // yes, this is in principle a bound, but it's not one we'd like to compile
+            bvs.Add(BoundVars[i]);
+          }
+        }
+      }
+      return bvs;
+    }
+
     public ComprehensionExpr(IToken tok, List<BoundVar> bvars, Expression range, Expression term, Attributes attrs)
       : base(tok) {
       Contract.Requires(tok != null);
diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index d82d7d1f..ec3a69c9 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -1313,16 +1313,6 @@ namespace Microsoft.Dafny
       }
     }
 
-    private readonly List<SetComprehension> needFiniteBoundsChecks_SetComprehension = new List<SetComprehension>();
-    private readonly List<AssignSuchThatStmt> needBoundsDiscovery_AssignSuchThatStmt = new List<AssignSuchThatStmt>();
-    private readonly List<LetExpr> needFiniteBoundsChecks_LetSuchThatExpr = new List<LetExpr>();
-    public int NFBC_Count {
-      // provided just for the purpose of conveniently writing contracts for ResolveTopLevelDecl_Meat
-      get {
-        return needFiniteBoundsChecks_SetComprehension.Count + needFiniteBoundsChecks_LetSuchThatExpr.Count;
-      }
-    }
-
     static readonly List<NativeType> NativeTypes = new List<NativeType>() {
       new NativeType("byte", 0, 0x100, "", true),
       new NativeType("sbyte", -0x80, 0x80, "", true),
@@ -1338,13 +1328,23 @@ namespace Microsoft.Dafny
       Contract.Requires(declarations != null);
       Contract.Requires(cce.NonNullElements(datatypeDependencies));
       Contract.Requires(cce.NonNullElements(codatatypeDependencies));
-      Contract.Requires(NFBC_Count == 0);
       Contract.Requires(AllTypeConstraints.Count == 0);
-      Contract.Ensures(NFBC_Count == 0);
       Contract.Ensures(AllTypeConstraints.Count == 0);
 
       int prevErrorCount = reporter.Count(ErrorLevel.Error);
 
+      // ---------------------------------- Pass 0 ----------------------------------
+      // This pass resolves names, introduces (and may solve) type constraints, and
+      // builds the module's call graph.
+      // Some bounds are discovered during this pass [is this necessary? can they be
+      // moved to pass 1 like the other bounds discovery? --KRML], namely:
+      //   - forall statements
+      //   - quantifier expressions
+      //   - map comprehensions
+      // For 'newtype' declarations, it also checks that all types were fully
+      // determined.
+      // ----------------------------------------------------------------------------
+
       // Resolve the meat of classes and iterators, the definitions of type synonyms, and the type parameters of all top-level type declarations
       // First, resolve the newtype declarations and the constraint clauses, including filling in .ResolvedOp fields.  This is needed for the
       // resolution of the other declarations, because those other declarations may invoke DiscoverBounds, which looks at the .Constraint field
@@ -1403,172 +1403,80 @@ namespace Microsoft.Dafny
         allTypeParameters.PopMarker();
       }
 
+      // ---------------------------------- Pass 1 ----------------------------------
+      // This pass:
+      // * checks that type inference was able to determine all types
+      // * fills in the .ResolvedOp field of binary expressions
+      // * discovers bounds for:
+      //     - set comprehensions
+      //     - assign-such-that statements
+      //     - compilable let-such-that expressions
+      //     - newtype constraints
+      // For each statement body that it successfully typed, this pass also:
+      // * computes ghost interests
+      // * determines/checks tail-recursion.
+      // ----------------------------------------------------------------------------
+
       Dictionary<string, NativeType> nativeTypeMap = new Dictionary<string, NativeType>();
       foreach (var nativeType in NativeTypes) {
         nativeTypeMap.Add(nativeType.Name, nativeType);
       }
-
       if (reporter.Count(ErrorLevel.Error) == prevErrorCount) {
         // Check that type inference went well everywhere; this will also fill in the .ResolvedOp field in binary expressions
         foreach (TopLevelDecl d in declarations) {
           if (d is IteratorDecl) {
             var iter = (IteratorDecl)d;
+            var prevErrCnt = reporter.Count(ErrorLevel.Error);
             iter.Members.Iter(CheckTypeInference_Member);
+            if (prevErrCnt == reporter.Count(ErrorLevel.Error)) {
+              iter.SubExpressions.Iter(e => CheckExpression(e, this, iter));
+            }
             if (iter.Body != null) {
               CheckTypeInference(iter.Body);
+              if (prevErrCnt == reporter.Count(ErrorLevel.Error)) {
+                ComputeGhostInterest(iter.Body, false, iter);
+                CheckExpression(iter.Body, this, iter);
+              }
             }
           } else if (d is ClassDecl) {
             var cl = (ClassDecl)d;
-            cl.Members.Iter(CheckTypeInference_Member);
             foreach (var member in cl.Members) {
-              var m = member as Method;
-              if (m != null && m.Body != null) {
-                DetermineTailRecursion(m);
+              var prevErrCnt = reporter.Count(ErrorLevel.Error);
+              CheckTypeInference_Member(member);
+              if (prevErrCnt == reporter.Count(ErrorLevel.Error)) {
+                if (member is Method) {
+                  var m = (Method)member;
+                  if (m.Body != null) {
+                    ComputeGhostInterest(m.Body, m.IsGhost, m);
+                    CheckExpression(m.Body, this, m);
+                    DetermineTailRecursion(m);
+                  }
+                } else if (member is Function) {
+                  var f = (Function)member;
+                  if (!f.IsGhost && f.Body != null) {
+                    CheckIsNonGhost(f.Body);
+                  }
+                  DetermineTailRecursion(f);
+                }
+                if (prevErrCnt == reporter.Count(ErrorLevel.Error) && member is ICodeContext) {
+                  member.SubExpressions.Iter(e => CheckExpression(e, this, (ICodeContext)member));
+                }
               }
             }
           } else if (d is NewtypeDecl) {
             var dd = (NewtypeDecl)d;
-            bool? boolNativeType = null;
-            NativeType stringNativeType = null;
-            object nativeTypeAttr = true;
-            bool hasNativeTypeAttr = Attributes.ContainsMatchingValue(dd.Attributes, "nativeType", ref nativeTypeAttr,
-              new Attributes.MatchingValueOption[] {
-                Attributes.MatchingValueOption.Empty,
-                Attributes.MatchingValueOption.Bool,
-                Attributes.MatchingValueOption.String },
-              err => reporter.Error(MessageSource.Resolver, dd, err));
-            if (hasNativeTypeAttr) {
-              if (nativeTypeAttr is bool) {
-                boolNativeType = (bool)nativeTypeAttr;
-              } else {
-                string keyString = (string)nativeTypeAttr;
-                if (nativeTypeMap.ContainsKey(keyString)) {
-                  stringNativeType = nativeTypeMap[keyString];
-                } else {
-                  reporter.Error(MessageSource.Resolver, dd, "Unsupported nativeType {0}", keyString);
-                }
-              }
-            }
-            if (stringNativeType != null || boolNativeType == true) {
-              if (!dd.BaseType.IsNumericBased(Type.NumericPersuation.Int)) {
-                reporter.Error(MessageSource.Resolver, dd, "nativeType can only be used on integral types");
-              }
-              if (dd.Var == null) {
-                reporter.Error(MessageSource.Resolver, dd, "nativeType can only be used if newtype specifies a constraint");
-              }
-            }
             if (dd.Var != null) {
               Contract.Assert(dd.Constraint != null);
-              CheckTypeInference(dd.Constraint);
-
-              Func<Expression, BigInteger?> GetConst = null;
-              GetConst = (Expression e) => {
-                int m = 1;
-                BinaryExpr bin = e as BinaryExpr;
-                if (bin != null && bin.Op == BinaryExpr.Opcode.Sub && GetConst(bin.E0) == BigInteger.Zero) {
-                  m = -1;
-                  e = bin.E1;
-                }
-                LiteralExpr l = e as LiteralExpr;
-                if (l != null && l.Value is BigInteger) {
-                  return m * (BigInteger)l.Value;
-                }
-                return null;
-              };
-              var bounds = DiscoverAllBounds_SingleVar(dd.Var, dd.Constraint);
-              List<NativeType> potentialNativeTypes =
-                (stringNativeType != null) ? new List<NativeType> { stringNativeType } :
-                (boolNativeType == false) ? new List<NativeType>() :
-                NativeTypes;
-              foreach (var nt in potentialNativeTypes) {
-                bool lowerOk = false;
-                bool upperOk = false;
-                foreach (var bound in bounds) {
-                  if (bound is ComprehensionExpr.IntBoundedPool) {
-                    var bnd = (ComprehensionExpr.IntBoundedPool)bound;
-                    if (bnd.LowerBound != null) {
-                      BigInteger? lower = GetConst(bnd.LowerBound);
-                      if (lower != null && nt.LowerBound <= lower) {
-                        lowerOk = true;
-                      }
-                    }
-                    if (bnd.UpperBound != null) {
-                      BigInteger? upper = GetConst(bnd.UpperBound);
-                      if (upper != null && upper <= nt.UpperBound) {
-                        upperOk = true;
-                      }
-                    }
-                  }
-                }
-                if (lowerOk && upperOk) {
-                  dd.NativeType = nt;
-                  break;
-                }
-              }
-              if (dd.NativeType == null && (boolNativeType == true || stringNativeType != null)) {
-                reporter.Error(MessageSource.Resolver, dd, "Dafny's heuristics cannot find a compatible native type.  " +
-                  "Hint: try writing a newtype constraint of the form 'i:int | lowerBound <= i < upperBound && (...any additional constraints...)'");
-              }
-              if (dd.NativeType != null && stringNativeType == null) {
-                reporter.Info(MessageSource.Resolver, dd.tok, "{:nativeType \"" + dd.NativeType.Name + "\"}");
-              }
+              CheckExpression(dd.Constraint, this, dd);
             }
+            FigureOutNativeType(dd, nativeTypeMap);
           }
         }
       }
 
-      if (reporter.Count(ErrorLevel.Error) == prevErrorCount) {
-        // At this point, it is necessary to know for each statement and expression if it is ghost or not
-        foreach (var e in needFiniteBoundsChecks_SetComprehension) {
-          CheckTypeInference(e.Range);  // we need to resolve operators before the call to DiscoverBounds
-          List<BoundVar> missingBounds;
-          e.Bounds = DiscoverBestBounds_MultipleVars(e.BoundVars, e.Range, true, true, out missingBounds);
-          if (missingBounds.Count != 0) {
-            e.MissingBounds = missingBounds;
-            if (e.Finite) {
-              foreach (var bv in e.MissingBounds) {
-                reporter.Error(MessageSource.Resolver, e, "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 '{0}'", bv.Name);
-              }
-            }
-          }
-        }
-        foreach (AssignSuchThatStmt s in needBoundsDiscovery_AssignSuchThatStmt) {
-          Contract.Assert(!s.IsGhost);
-          var varLhss = new List<IVariable>();
-          foreach (var lhs in s.Lhss) {
-            var ide = (IdentifierExpr)lhs.Resolved;  // successful resolution above implies all LHS's are IdentifierExpr's
-            varLhss.Add(ide.Var);
-          }
-
-          List<IVariable> missingBounds;
-          var bestBounds = DiscoverBestBounds_MultipleVars(varLhss, s.Expr, true, false, out missingBounds);
-          if (missingBounds.Count != 0) {
-            s.MissingBounds = missingBounds;  // so that an error message can be produced during compilation
-          } else {
-            Contract.Assert(bestBounds != null);
-            s.Bounds = bestBounds;
-          }
-        }
-        foreach (var e in needFiniteBoundsChecks_LetSuchThatExpr) {
-          Contract.Assert(!e.Exact);  // only let-such-that expressions are ever added to the list
-          Contract.Assert(e.RHSs.Count == 1);  // if we got this far, the resolver will have checked this condition successfully
-          var constraint = e.RHSs[0];
-          CheckTypeInference(constraint);  // we need to resolve operators before the call to DiscoverBounds
-          List<IVariable> missingBounds;
-          var vars = new List<IVariable>(e.BoundVars);
-          var bestBounds = DiscoverBestBounds_MultipleVars(vars, constraint, true, false, out missingBounds);
-          if (missingBounds.Count != 0) {
-            e.Constraint_MissingBounds = missingBounds;
-            foreach (var bv in e.Constraint_MissingBounds) {
-              reporter.Error(MessageSource.Resolver, e, "a non-ghost let-such-that constraint must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{0}'", bv.Name);
-            }
-          } else {
-            e.Constraint_Bounds = bestBounds;
-          }
-        }
-      }
-      needFiniteBoundsChecks_SetComprehension.Clear();
-      needFiniteBoundsChecks_LetSuchThatExpr.Clear();
+      // ---------------------------------- Pass 2 ----------------------------------
+      // This pass fills in various additional information.
+      // ----------------------------------------------------------------------------
 
       if (reporter.Count(ErrorLevel.Error) == prevErrorCount) {
         // fill in the postconditions and bodies of prefix lemmas
@@ -1894,6 +1802,93 @@ namespace Microsoft.Dafny
       }
     }
 
+    private void FigureOutNativeType(NewtypeDecl dd, Dictionary<string, NativeType> nativeTypeMap) {
+      Contract.Requires(dd != null);
+      Contract.Requires(nativeTypeMap != null);
+      bool? boolNativeType = null;
+      NativeType stringNativeType = null;
+      object nativeTypeAttr = true;
+      bool hasNativeTypeAttr = Attributes.ContainsMatchingValue(dd.Attributes, "nativeType", ref nativeTypeAttr,
+        new Attributes.MatchingValueOption[] {
+                Attributes.MatchingValueOption.Empty,
+                Attributes.MatchingValueOption.Bool,
+                Attributes.MatchingValueOption.String },
+        err => reporter.Error(MessageSource.Resolver, dd, err));
+      if (hasNativeTypeAttr) {
+        if (nativeTypeAttr is bool) {
+          boolNativeType = (bool)nativeTypeAttr;
+        } else {
+          string keyString = (string)nativeTypeAttr;
+          if (nativeTypeMap.ContainsKey(keyString)) {
+            stringNativeType = nativeTypeMap[keyString];
+          } else {
+            reporter.Error(MessageSource.Resolver, dd, "Unsupported nativeType {0}", keyString);
+          }
+        }
+      }
+      if (stringNativeType != null || boolNativeType == true) {
+        if (!dd.BaseType.IsNumericBased(Type.NumericPersuation.Int)) {
+          reporter.Error(MessageSource.Resolver, dd, "nativeType can only be used on integral types");
+        }
+        if (dd.Var == null) {
+          reporter.Error(MessageSource.Resolver, dd, "nativeType can only be used if newtype specifies a constraint");
+        }
+      }
+      if (dd.Var != null) {
+        Func<Expression, BigInteger?> GetConst = null;
+        GetConst = (Expression e) => {
+          int m = 1;
+          BinaryExpr bin = e as BinaryExpr;
+          if (bin != null && bin.Op == BinaryExpr.Opcode.Sub && GetConst(bin.E0) == BigInteger.Zero) {
+            m = -1;
+            e = bin.E1;
+          }
+          LiteralExpr l = e as LiteralExpr;
+          if (l != null && l.Value is BigInteger) {
+            return m * (BigInteger)l.Value;
+          }
+          return null;
+        };
+        var bounds = DiscoverAllBounds_SingleVar(dd.Var, dd.Constraint);
+        List<NativeType> potentialNativeTypes =
+          (stringNativeType != null) ? new List<NativeType> { stringNativeType } :
+          (boolNativeType == false) ? new List<NativeType>() :
+          NativeTypes;
+        foreach (var nt in potentialNativeTypes) {
+          bool lowerOk = false;
+          bool upperOk = false;
+          foreach (var bound in bounds) {
+            if (bound is ComprehensionExpr.IntBoundedPool) {
+              var bnd = (ComprehensionExpr.IntBoundedPool)bound;
+              if (bnd.LowerBound != null) {
+                BigInteger? lower = GetConst(bnd.LowerBound);
+                if (lower != null && nt.LowerBound <= lower) {
+                  lowerOk = true;
+                }
+              }
+              if (bnd.UpperBound != null) {
+                BigInteger? upper = GetConst(bnd.UpperBound);
+                if (upper != null && upper <= nt.UpperBound) {
+                  upperOk = true;
+                }
+              }
+            }
+          }
+          if (lowerOk && upperOk) {
+            dd.NativeType = nt;
+            break;
+          }
+        }
+        if (dd.NativeType == null && (boolNativeType == true || stringNativeType != null)) {
+          reporter.Error(MessageSource.Resolver, dd, "Dafny's heuristics cannot find a compatible native type.  " +
+            "Hint: try writing a newtype constraint of the form 'i:int | lowerBound <= i < upperBound && (...any additional constraints...)'");
+        }
+        if (dd.NativeType != null && stringNativeType == null) {
+          reporter.Info(MessageSource.Resolver, dd.tok, "{:nativeType \"" + dd.NativeType.Name + "\"}");
+        }
+      }
+    }
+
     /// <summary>
     /// Adds the type constraint ty==expected, eventually printing the error message "msg" if this is found to be
     /// untenable.  If this is immediately known not to be untenable, false is returned.
@@ -2123,16 +2118,60 @@ namespace Microsoft.Dafny
         } else if (stmt is ForallStmt) {
           var s = (ForallStmt)stmt;
           s.BoundVars.Iter(bv => CheckTypeIsDetermined(bv.tok, bv.Type, "bound variable"));
+        } else if (stmt is AssignSuchThatStmt) {
+          var s = (AssignSuchThatStmt)stmt;
+          if (s.AssumeToken == null) {
+            var varLhss = new List<IVariable>();
+            foreach (var lhs in s.Lhss) {
+              var ide = (IdentifierExpr)lhs.Resolved;  // successful resolution implies all LHS's are IdentifierExpr's
+              varLhss.Add(ide.Var);
+            }
+            List<IVariable> missingBounds;
+            var bestBounds = DiscoverBestBounds_MultipleVars(varLhss, s.Expr, true, false, out missingBounds);
+            if (missingBounds.Count != 0) {
+              s.MissingBounds = missingBounds;  // so that an error message can be produced during compilation
+            } else {
+              Contract.Assert(bestBounds != null);
+              s.Bounds = bestBounds;
+            }
+          }
+        } else if (stmt is CalcStmt) {
+          var s = (CalcStmt)stmt;
+          // The resolution of the calc statement builds up .Steps and .Result, which are of the form E0 OP E1, where
+          // E0 and E1 are expressions from .Lines.  These additional expressions still need to have their .ResolvedOp
+          // fields filled in, so we visit them (but not their subexpressions) here.
+          foreach (var e in s.Steps) {
+            VisitOneExpr(e);
+          }
+          VisitOneExpr(s.Result);
         }
       }
       protected override void VisitOneExpr(Expression expr) {
         if (expr is ComprehensionExpr) {
           var e = (ComprehensionExpr)expr;
-          if (e != null) {
-            foreach (var bv in e.BoundVars) {
-              if (!IsDetermined(bv.Type.Normalize())) {
-                resolver.reporter.Error(MessageSource.Resolver, bv.tok, "type of bound variable '{0}' could not be determined; please specify the type explicitly",
-                  bv.Name);
+          foreach (var bv in e.BoundVars) {
+            if (!IsDetermined(bv.Type.Normalize())) {
+              resolver.reporter.Error(MessageSource.Resolver, bv.tok, "type of bound variable '{0}' could not be determined; please specify the type explicitly", bv.Name);
+            }
+          }
+          if (e is SetComprehension) {
+            var sc = (SetComprehension)e;
+            if (sc.Finite) {
+              // A set must be finite.  Discover bounds for the Range expression, but report an error only if the Term is not
+              // of a finite-individuals type.
+              List<BoundVar> missingBounds;
+              sc.Bounds = DiscoverBestBounds_MultipleVars(sc.BoundVars, sc.Range, true, true, out missingBounds);
+              if (missingBounds.Count != 0) {
+                sc.MissingBounds = missingBounds;
+                if (sc.Type.HasFinitePossibleValues) {
+                  // This means the set is finite, regardless of if the Range is bounded.  So, we don't give any error here.
+                  // However, if this expression is used in a non-ghost context (which is not yet known at this stage of
+                  // resolution), the resolver will generate an error about that later.
+                } else {
+                  foreach (var bv in sc.MissingBounds) {
+                    resolver.reporter.Error(MessageSource.Resolver, sc, "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 '{0}'", bv.Name);
+                  }
+                }
               }
             }
           }
@@ -2172,6 +2211,7 @@ namespace Microsoft.Dafny
           var bin = expr as BinaryExpr;
           if (bin != null) {
             bin.ResolvedOp = ResolveOp(bin.Op, bin.E1.Type);
+          
           }
         }
       }
@@ -2250,6 +2290,58 @@ namespace Microsoft.Dafny
     #endregion CheckTypeInference
 
     // ------------------------------------------------------------------------------------------------------
+    // ----- CheckExpression --------------------------------------------------------------------------------
+    // ------------------------------------------------------------------------------------------------------
+    #region CheckExpression
+    /// <summary>
+    /// This method computes ghost interests in the statement portion of StmtExpr's and
+    /// checks for hint restrictions in any CalcStmt.
+    /// </summary>
+    void CheckExpression(Expression expr, Resolver resolver, ICodeContext codeContext) {
+      Contract.Requires(expr != null);
+      Contract.Requires(resolver != null);
+      Contract.Requires(codeContext != null);
+      var v = new CheckExpression_Visitor(resolver, codeContext);
+      v.Visit(expr);
+    }
+    /// <summary>
+    /// This method computes ghost interests in the statement portion of StmtExpr's and
+    /// checks for hint restrictions in any CalcStmt.
+    /// </summary>
+    void CheckExpression(Statement stmt, Resolver resolver, ICodeContext codeContext) {
+      Contract.Requires(stmt != null);
+      Contract.Requires(resolver != null);
+      Contract.Requires(codeContext != null);
+      var v = new CheckExpression_Visitor(resolver, codeContext);
+      v.Visit(stmt);
+    }
+    class CheckExpression_Visitor : ResolverBottomUpVisitor
+    {
+      readonly ICodeContext CodeContext;
+      public CheckExpression_Visitor(Resolver resolver, ICodeContext codeContext)
+        : base(resolver) {
+        Contract.Requires(resolver != null);
+        Contract.Requires(codeContext != null);
+        CodeContext = codeContext;
+      }
+      protected override void VisitOneExpr(Expression expr) {
+        if (expr is StmtExpr) {
+          var e = (StmtExpr)expr;
+          resolver.ComputeGhostInterest(e.S, true, CodeContext);
+        }
+      }
+      protected override void VisitOneStmt(Statement stmt) {
+        if (stmt is CalcStmt) {
+          var s = (CalcStmt)stmt;
+          foreach (var h in s.Hints) {
+            resolver.CheckHintRestrictions(h, new HashSet<LocalVariable>());
+          }
+        }
+      }
+    }
+    #endregion
+
+    // ------------------------------------------------------------------------------------------------------
     // ----- CheckTailRecursive -----------------------------------------------------------------------------
     // ------------------------------------------------------------------------------------------------------
     #region CheckTailRecursive
@@ -3009,11 +3101,11 @@ namespace Microsoft.Dafny
     // ----- ComputeGhostInterest ---------------------------------------------------------------------------
     // ------------------------------------------------------------------------------------------------------
     #region ComputeGhostInterest
-    public void ComputeGhostInterest(Statement stmt, ICodeContext codeContext) {
+    public void ComputeGhostInterest(Statement stmt, bool mustBeErasable, ICodeContext codeContext) {
       Contract.Requires(stmt != null);
       Contract.Requires(codeContext != null);
       var visitor = new GhostInterest_Visitor(codeContext, this);
-      visitor.Visit(stmt, codeContext.IsGhost);
+      visitor.Visit(stmt, mustBeErasable);
     }
     class GhostInterest_Visitor
     {
@@ -3037,12 +3129,6 @@ namespace Microsoft.Dafny
         Contract.Requires(msgArgs != null);
         resolver.reporter.Error(MessageSource.Resolver, expr, msg, msgArgs);
       }
-      protected void Error(IToken tok, string msg, params object[] msgArgs) {
-        Contract.Requires(tok != null);
-        Contract.Requires(msg != null);
-        Contract.Requires(msgArgs != null);
-        resolver.reporter.Error(MessageSource.Resolver, tok, msg, msgArgs);
-      }
       /// <summary>
       /// This method does three things:
       /// 0. Reports an error if "mustBeErasable" and the statement assigns to a non-ghost field
@@ -3057,6 +3143,7 @@ namespace Microsoft.Dafny
       /// because break statements look at the ghost status of its enclosing statements.
       /// </summary>
       public void Visit(Statement stmt, bool mustBeErasable) {
+        Contract.Requires(stmt != null);
         Contract.Assume(!codeContext.IsGhost || mustBeErasable);  // (this is really a precondition) codeContext.IsGhost ==> mustBeErasable
 
         if (stmt is PredicateStmt) {
@@ -3107,9 +3194,6 @@ namespace Microsoft.Dafny
               }
             }
           }
-          if (!s.IsGhost) {
-            resolver.needBoundsDiscovery_AssignSuchThatStmt.Add(s);
-          }
 
         } else if (stmt is UpdateStmt) {
           var s = (UpdateStmt)stmt;
@@ -3124,13 +3208,6 @@ namespace Microsoft.Dafny
               local.IsGhost = true;
             }
           }
-          foreach (var local in s.Locals) {
-            if (Attributes.Contains(local.Attributes, "assumption")) {
-              if (!local.IsGhost) {
-                Error(local.Tok, "assumption variable must be ghost");
-              }
-            }
-          }
           s.IsGhost = (s.Update == null || s.Update.IsGhost) && s.Locals.All(v => v.IsGhost);
           if (s.Update != null) {
             Visit(s.Update, mustBeErasable);
@@ -4040,14 +4117,10 @@ namespace Microsoft.Dafny
         var prevErrorCount = reporter.Count(ErrorLevel.Error);
         ResolveExpression(f.Body, new ResolveOpts(f, false));
         SolveAllTypeConstraints();
-        if (!f.IsGhost && prevErrorCount == reporter.Count(ErrorLevel.Error)) {
-          CheckIsNonGhost(f.Body);
-        }
         Contract.Assert(f.Body.Type != null);  // follows from postcondition of ResolveExpression
         ConstrainTypes(f.Body.Type, f.ResultType, f, "Function body type mismatch (expected {0}, got {1})", f.ResultType, f.Body.Type);
       }
       scope.PopMarker();
-      DetermineTailRecursion(f);
     }
 
     /// <summary>
@@ -4187,7 +4260,7 @@ namespace Microsoft.Dafny
           ResolveBlockStatement(m.Body, m.IsGhost, m);
           SolveAllTypeConstraints();
           if (reporter.Count(ErrorLevel.Error) == prevErrorCount) {
-            ComputeGhostInterest(m.Body, m);
+//KRML            ComputeGhostInterest(m.Body, m);
           }
         }
 
@@ -4308,7 +4381,7 @@ namespace Microsoft.Dafny
       if (iter.Body != null) {
         ResolveBlockStatement(iter.Body, false, iter);
         if (reporter.Count(ErrorLevel.Error) == postSpecErrorCount) {
-          ComputeGhostInterest(iter.Body, iter);
+          //KRML          ComputeGhostInterest(iter.Body, iter);
         }
       }
 
@@ -5290,7 +5363,10 @@ namespace Microsoft.Dafny
             }
             if (!(local.Type.IsBoolType))
             {
-              reporter.Error(MessageSource.Resolver, s, "assumption variable must be of type 'bool'");
+              reporter.Error(MessageSource.Resolver, local.Tok, "assumption variable must be of type 'bool'");
+            }
+            if (!local.IsGhost) {
+              reporter.Error(MessageSource.Resolver, local.Tok, "assumption variable must be ghost");
             }
           }
         }
@@ -5599,7 +5675,6 @@ namespace Microsoft.Dafny
           loopStack = new List<Statement>();
           foreach (var h in s.Hints) {
             ResolveStatement(h, true, codeContext);
-            CheckHintRestrictions(h);
           }
           labeledStatements = prevLblStmts;
           loopStack = prevLoopStack;
@@ -6347,9 +6422,6 @@ namespace Microsoft.Dafny
       if (!isInitCall && callee is Constructor) {
         reporter.Error(MessageSource.Resolver, s, "a constructor is allowed to be called only when an object is being allocated");
       }
-      if (specContextOnly && !callee.IsGhost) {
-        reporter.Error(MessageSource.Resolver, s, "only ghost methods can be called from this context");
-      }
 
       // resolve left-hand sides
       foreach (var lhs in s.Lhs) {
@@ -6633,8 +6705,9 @@ namespace Microsoft.Dafny
     /// Check that a statment is a valid hint for a calculation.
     /// ToDo: generalize the part for compound statements to take a delegate?
     /// </summary>
-    public void CheckHintRestrictions(Statement stmt) {
+    public void CheckHintRestrictions(Statement stmt, ISet<LocalVariable> localsAllowedInUpdates) {
       Contract.Requires(stmt != null);
+      Contract.Requires(localsAllowedInUpdates != null);
       if (stmt is PredicateStmt) {
         // cool
       } else if (stmt is PrintStmt) {
@@ -6648,11 +6721,11 @@ namespace Microsoft.Dafny
       } else if (stmt is AssignSuchThatStmt) {
         var s = (AssignSuchThatStmt)stmt;
         foreach (var lhs in s.Lhss) {
-          CheckHintLhs(s.Tok, lhs.Resolved);
+          CheckHintLhs(s.Tok, lhs.Resolved, localsAllowedInUpdates);
         }
       } else if (stmt is AssignStmt) {
         var s = (AssignStmt)stmt;
-        CheckHintLhs(s.Tok, s.Lhs.Resolved);
+        CheckHintLhs(s.Tok, s.Lhs.Resolved, localsAllowedInUpdates);
       } else if (stmt is CallStmt) {
         var s = (CallStmt)stmt;
         if (s.Method.Mod.Expressions.Count != 0) {
@@ -6661,33 +6734,33 @@ namespace Microsoft.Dafny
       } else if (stmt is UpdateStmt) {
         var s = (UpdateStmt)stmt;
         foreach (var ss in s.ResolvedStatements) {
-          CheckHintRestrictions(ss);
+          CheckHintRestrictions(ss, localsAllowedInUpdates);
         }
       } else if (stmt is VarDeclStmt) {
         var s = (VarDeclStmt)stmt;
+        s.Locals.Iter(local => localsAllowedInUpdates.Add(local));
         if (s.Update != null) {
-          CheckHintRestrictions(s.Update);
+          CheckHintRestrictions(s.Update, localsAllowedInUpdates);
         }
       } else if (stmt is BlockStmt) {
         var s = (BlockStmt)stmt;
-        scope.PushMarker();
+        var newScopeForLocals = new HashSet<LocalVariable>(localsAllowedInUpdates);
         foreach (var ss in s.Body) {
-          CheckHintRestrictions(ss);
+          CheckHintRestrictions(ss, newScopeForLocals);
         }
-        scope.PopMarker();
 
       } else if (stmt is IfStmt) {
         var s = (IfStmt)stmt;
-        CheckHintRestrictions(s.Thn);
+        CheckHintRestrictions(s.Thn, localsAllowedInUpdates);
         if (s.Els != null) {
-          CheckHintRestrictions(s.Els);
+          CheckHintRestrictions(s.Els, localsAllowedInUpdates);
         }
 
       } else if (stmt is AlternativeStmt) {
         var s = (AlternativeStmt)stmt;
         foreach (var alt in s.Alternatives) {
           foreach (var ss in alt.Body) {
-            CheckHintRestrictions(ss);
+            CheckHintRestrictions(ss, localsAllowedInUpdates);
           }
         }
 
@@ -6697,14 +6770,14 @@ namespace Microsoft.Dafny
           reporter.Error(MessageSource.Resolver, s.Mod.Expressions[0].tok, "a while statement used inside a hint is not allowed to have a modifies clause");
         }
         if (s.Body != null) {
-          CheckHintRestrictions(s.Body);
+          CheckHintRestrictions(s.Body, localsAllowedInUpdates);
         }
 
       } else if (stmt is AlternativeLoopStmt) {
         var s = (AlternativeLoopStmt)stmt;
         foreach (var alt in s.Alternatives) {
           foreach (var ss in alt.Body) {
-            CheckHintRestrictions(ss);
+            CheckHintRestrictions(ss, localsAllowedInUpdates);
           }
         }
 
@@ -6726,14 +6799,14 @@ namespace Microsoft.Dafny
       } else if (stmt is CalcStmt) {
         var s = (CalcStmt)stmt;
         foreach (var h in s.Hints) {
-          CheckHintRestrictions(h);
+          CheckHintRestrictions(h, new HashSet<LocalVariable>());
         }
 
       } else if (stmt is MatchStmt) {
         var s = (MatchStmt)stmt;
         foreach (var kase in s.Cases) {
           foreach (var ss in kase.Body) {
-            CheckHintRestrictions(ss);
+            CheckHintRestrictions(ss, localsAllowedInUpdates);
           }
         }
 
@@ -6742,11 +6815,14 @@ namespace Microsoft.Dafny
       }
     }
 
-    void CheckHintLhs(IToken tok, Expression lhs) {
+    void CheckHintLhs(IToken tok, Expression lhs, ISet<LocalVariable> localsAllowedInUpdates) {
+      Contract.Requires(tok != null);
+      Contract.Requires(lhs != null);
+      Contract.Requires(localsAllowedInUpdates != null);
       var idExpr = lhs as IdentifierExpr;
       if (idExpr == null) {
         reporter.Error(MessageSource.Resolver, tok, "a hint is not allowed to update heap locations");
-      } else if (scope.ContainsDecl(idExpr.Var)) {
+      } else if (!localsAllowedInUpdates.Contains(idExpr.Var)) {
         reporter.Error(MessageSource.Resolver, tok, "a hint is not allowed to update a variable declared outside the hint");
       }
     }
@@ -7768,9 +7844,6 @@ namespace Microsoft.Dafny
             ResolveExpression(rhs, opts);
             ConstrainTypes(rhs.Type, Type.Bool, rhs.tok, "type of RHS of let-such-that expression must be boolean (got {0})", rhs.Type);
           }
-          if (!opts.DontCareAboutCompilation && !e.BoundVars.All(bv => bv.IsGhost)) {
-            needFiniteBoundsChecks_LetSuchThatExpr.Add(e);
-          }
         }
         ResolveExpression(e.Body, opts);
         ResolveAttributes(e.Attributes, new ResolveOpts(opts, true));
@@ -7819,21 +7892,17 @@ namespace Microsoft.Dafny
           List<BoundVar> missingBounds;
           e.Bounds = DiscoverBestBounds_MultipleVars(e.BoundVars, e.LogicalBody(), e is ExistsExpr, true, out missingBounds);
           if (missingBounds.Count != 0) {
-            // Report errors here about quantifications that depend on the allocation state.
-            var mb = missingBounds;
-            if (opts.codeContext is Function) {
-              mb = new List<BoundVar>();  // (who cares if we allocate another array; this happens only in the case of a resolution error anyhow)
-              foreach (var bv in missingBounds) {
-                if (bv.Type.IsRefType) {
-                  reporter.Error(MessageSource.Resolver, expr, "a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of '{0}'", bv.Name);
-                } else {
-                  mb.Add(bv);
-                }
+            e.MissingBounds = missingBounds;
+          }
+          if (opts.codeContext is Function && e.Bounds != null) {
+            Contract.Assert(e.Bounds.Count == e.BoundVars.Count);
+            for (int i = 0; i < e.Bounds.Count; i++) {
+              var bound = e.Bounds[i] as ComprehensionExpr.RefBoundedPool;
+              if (bound != null) {
+                var bv = e.BoundVars[i];
+                reporter.Error(MessageSource.Resolver, expr, "a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of '{0}'", bv.Name);
               }
             }
-            if (mb.Count != 0) {
-              e.MissingBounds = mb;
-            }
           }
         }
 
@@ -7855,12 +7924,6 @@ namespace Microsoft.Dafny
         scope.PopMarker();
         expr.Type = new SetType(e.Finite, e.Term.Type);
 
-        if (opts.DontCareAboutCompilation && (e.Term.Type.IsRefType || e.Term.Type.IsBoolType) || e.Term.Type.IsCharType) {
-          // ok, term type is finite and we're in a ghost context
-        } else {
-          needFiniteBoundsChecks_SetComprehension.Add(e);
-        }
-
       } else if (expr is MapComprehension) {
         var e = (MapComprehension)expr;
         int prevErrorCount = reporter.Count(ErrorLevel.Error);
@@ -9329,17 +9392,47 @@ namespace Microsoft.Dafny
             CheckIsNonGhost(e.RHSs[0]);
           }
           CheckIsNonGhost(e.Body);
+
+          // fill in bounds for this to-be-compiled let-such-that expression
+          Contract.Assert(e.RHSs.Count == 1);  // if we got this far, the resolver will have checked this condition successfully
+          var constraint = e.RHSs[0];
+          List<IVariable> missingBounds;
+          var vars = new List<IVariable>(e.BoundVars);
+          var bestBounds = DiscoverBestBounds_MultipleVars(vars, constraint, true, false, out missingBounds);
+          if (missingBounds.Count != 0) {
+            e.Constraint_MissingBounds = missingBounds;
+            foreach (var bv in e.Constraint_MissingBounds) {
+              reporter.Error(MessageSource.Resolver, e, "a non-ghost let-such-that constraint must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{0}'", bv.Name);
+            }
+          } else {
+            e.Constraint_Bounds = bestBounds;
+          }
         }
         return;
-      } else if (expr is QuantifierExpr) {
-        var e = (QuantifierExpr)expr;
-        Contract.Assert(e.SplitQuantifier == null); // No split quantifiers during resolution
-        if (e.MissingBounds != null) {
-          foreach (var bv in e.MissingBounds) {
-            reporter.Error(MessageSource.Resolver, expr, "quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for '{0}'", bv.Name);
+      } else if (expr is LambdaExpr) {
+        var e = expr as LambdaExpr;
+        CheckIsNonGhost(e.Body);
+        return;
+      } else if (expr is ComprehensionExpr) {
+        var e = (ComprehensionExpr)expr;
+        var uncompilableBoundVars = e.UncompilableBoundVars();
+        if (uncompilableBoundVars.Count != 0) {
+          string what;
+          if (e is SetComprehension) {
+            what = "set comprehensions";
+          } else if (e is MapComprehension) {
+            what = "map comprehensions";
+          } else {
+            Contract.Assume(e is QuantifierExpr);  // otherwise, unexpected ComprehensionExpr (since LambdaExpr is handled separately above)
+            Contract.Assert(((QuantifierExpr)e).SplitQuantifier == null); // No split quantifiers during resolution
+            what = "quantifiers";
+          }
+          foreach (var bv in uncompilableBoundVars) {
+            reporter.Error(MessageSource.Resolver, expr, "{0} 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 '{1}'", what, bv.Name);
           }
           return;
         }
+
       } else if (expr is MapComprehension) {
         var e = (MapComprehension)expr;
         if (e.MissingBounds != null && !e.Finite) {
@@ -9358,10 +9451,6 @@ namespace Microsoft.Dafny
         var e = (ChainingExpression)expr;
         e.Operands.ForEach(CheckIsNonGhost);
         return;
-      } else if (expr is LambdaExpr) {
-        var e = expr as LambdaExpr;
-        CheckIsNonGhost(e.Body);
-        return;
       }
 
       foreach (var ee in expr.SubExpressions) {
@@ -9520,8 +9609,11 @@ namespace Microsoft.Dafny
 
       // Maybe the type itself gives a bound
       if (bv.Type.IsBoolType) {
-        // easy
         bounds.Add(new ComprehensionExpr.BoolBoundedPool());
+      } else if (bv.Type.IsCharType) {
+        bounds.Add(new ComprehensionExpr.CharBoundedPool());
+      } else if (bv.Type.IsRefType) {
+        bounds.Add(new ComprehensionExpr.RefBoundedPool(bv.Type));
       } else if (bv.Type.IsIndDatatype && bv.Type.AsIndDatatype.HasFinitePossibleValues) {
         bounds.Add(new ComprehensionExpr.DatatypeBoundedPool(bv.Type.AsIndDatatype));
       } else if (bv.Type.IsNumericBased(Type.NumericPersuation.Int)) {
diff --git a/Test/dafny0/AssumptionVariables0.dfy.expect b/Test/dafny0/AssumptionVariables0.dfy.expect
index 16572961..83eb8a73 100644
--- a/Test/dafny0/AssumptionVariables0.dfy.expect
+++ b/Test/dafny0/AssumptionVariables0.dfy.expect
@@ -1,13 +1,13 @@
 AssumptionVariables0.dfy(6,29): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && <boolean expression>"
 AssumptionVariables0.dfy(7,33): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a2 && <boolean expression>"
-AssumptionVariables0.dfy(9,2): Error: assumption variable must be of type 'bool'
+AssumptionVariables0.dfy(9,26): Error: assumption variable must be of type 'bool'
 AssumptionVariables0.dfy(15,5): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a3 && <boolean expression>"
 AssumptionVariables0.dfy(17,5): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a3 && <boolean expression>"
 AssumptionVariables0.dfy(27,5): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && <boolean expression>"
 AssumptionVariables0.dfy(31,5): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && <boolean expression>"
 AssumptionVariables0.dfy(53,9): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && <boolean expression>"
 AssumptionVariables0.dfy(61,37): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && <boolean expression>"
-AssumptionVariables0.dfy(61,10): Error: assumption variable must be of type 'bool'
+AssumptionVariables0.dfy(61,34): Error: assumption variable must be of type 'bool'
 AssumptionVariables0.dfy(69,15): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && <boolean expression>"
 AssumptionVariables0.dfy(78,20): Error: assumption variable must be ghost
 12 resolution/type errors detected in AssumptionVariables0.dfy
diff --git a/Test/dafny0/CallStmtTests.dfy b/Test/dafny0/CallStmtTests.dfy
index 67e66b34..46c466ff 100644
--- a/Test/dafny0/CallStmtTests.dfy
+++ b/Test/dafny0/CallStmtTests.dfy
@@ -1,23 +1,27 @@
 // RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
-method testing1(t: int)
-{
-   t := m(); // error: should be checked at the Dafny level, not fall to Boogie.
-}
+module M0 {
+  method testing1(t: int)
+ {
+    t := m(); // error: should be checked at the Dafny level, not fall to Boogie.
+  }
 
-method m() returns (r: int)
-{
-   return 3;
+  method m() returns (r: int)
+  {
+    return 3;
+  }
 }
 
-method testing2()
-{
-   var v;
-   v := m2(); // error: v needs to be ghost because r is.
-}
+module M1 {
+  method testing2()
+  {
+    var v;
+    v := m2(); // error: v needs to be ghost because r is.
+  }
 
-method m2() returns (ghost r: int)
-{
-   r := 23;
+  method m2() returns (ghost r: int)
+  {
+    r := 23;
+  }
 }
diff --git a/Test/dafny0/CallStmtTests.dfy.expect b/Test/dafny0/CallStmtTests.dfy.expect
index 8a334754..246b89f8 100644
--- a/Test/dafny0/CallStmtTests.dfy.expect
+++ b/Test/dafny0/CallStmtTests.dfy.expect
@@ -1,3 +1,3 @@
-CallStmtTests.dfy(6,3): Error: LHS of assignment must denote a mutable variable
-CallStmtTests.dfy(17,10): Error: actual out-parameter 0 is required to be a ghost variable
+CallStmtTests.dfy(7,4): Error: LHS of assignment must denote a mutable variable
+CallStmtTests.dfy(20,11): Error: actual out-parameter 0 is required to be a ghost variable
 2 resolution/type errors detected in CallStmtTests.dfy
diff --git a/Test/dafny0/DiscoverBounds.dfy.expect b/Test/dafny0/DiscoverBounds.dfy.expect
index ee816683..34003053 100644
--- a/Test/dafny0/DiscoverBounds.dfy.expect
+++ b/Test/dafny0/DiscoverBounds.dfy.expect
@@ -1,4 +1,4 @@
-DiscoverBounds.dfy(36,7): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'o''
-DiscoverBounds.dfy(39,7): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'r'
-DiscoverBounds.dfy(40,7): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'r''
+DiscoverBounds.dfy(36,7): Error: quantifiers 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''
+DiscoverBounds.dfy(39,7): Error: quantifiers 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 'r'
+DiscoverBounds.dfy(40,7): Error: quantifiers 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 'r''
 3 resolution/type errors detected in DiscoverBounds.dfy
diff --git a/Test/dafny0/NonGhostQuantifiers.dfy b/Test/dafny0/NonGhostQuantifiers.dfy
index bff1d65b..e522d0fc 100644
--- a/Test/dafny0/NonGhostQuantifiers.dfy
+++ b/Test/dafny0/NonGhostQuantifiers.dfy
@@ -181,6 +181,12 @@ module DependencyOnAllAllocatedObjects {
     forall c: SomeClass :: true  // error: not allowed to dependend on which objects are allocated
   }
 
+  class SomeClass {
+    var f: int;
+  }
+}
+
+module DependencyOnAllAllocatedObjects_More {
   method M()
   {
     var b := forall c: SomeClass :: c != null ==> c.f == 0;  // error: non-ghost code requires bounds
@@ -192,3 +198,4 @@ module DependencyOnAllAllocatedObjects {
     var f: int;
   }
 }
+
diff --git a/Test/dafny0/NonGhostQuantifiers.dfy.expect b/Test/dafny0/NonGhostQuantifiers.dfy.expect
index 1e2fce17..6b737add 100644
--- a/Test/dafny0/NonGhostQuantifiers.dfy.expect
+++ b/Test/dafny0/NonGhostQuantifiers.dfy.expect
@@ -6,16 +6,16 @@ NonGhostQuantifiers.dfy(167,4): Error: a quantifier involved in a function defin
 NonGhostQuantifiers.dfy(171,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'
 NonGhostQuantifiers.dfy(176,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'
 NonGhostQuantifiers.dfy(181,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'
-NonGhostQuantifiers.dfy(186,13): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'c'
-NonGhostQuantifiers.dfy(16,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n'
-NonGhostQuantifiers.dfy(45,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n'
-NonGhostQuantifiers.dfy(49,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'd'
-NonGhostQuantifiers.dfy(53,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n'
-NonGhostQuantifiers.dfy(77,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'i'
-NonGhostQuantifiers.dfy(81,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'
-NonGhostQuantifiers.dfy(91,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'
-NonGhostQuantifiers.dfy(106,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'
-NonGhostQuantifiers.dfy(114,10): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'y'
-NonGhostQuantifiers.dfy(123,8): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'x'
+NonGhostQuantifiers.dfy(192,13): Error: quantifiers 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 'c'
+NonGhostQuantifiers.dfy(16,5): Error: quantifiers 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 'n'
+NonGhostQuantifiers.dfy(45,4): Error: quantifiers 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 'n'
+NonGhostQuantifiers.dfy(49,4): Error: quantifiers 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 'd'
+NonGhostQuantifiers.dfy(53,4): Error: quantifiers 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 'n'
+NonGhostQuantifiers.dfy(77,5): Error: quantifiers 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 'i'
+NonGhostQuantifiers.dfy(81,5): Error: quantifiers 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 'j'
+NonGhostQuantifiers.dfy(91,5): Error: quantifiers 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 'j'
+NonGhostQuantifiers.dfy(106,5): Error: quantifiers 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 'j'
+NonGhostQuantifiers.dfy(114,10): Error: quantifiers 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 'y'
+NonGhostQuantifiers.dfy(123,8): Error: quantifiers 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 'x'
 NonGhostQuantifiers.dfy(140,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
 20 resolution/type errors detected in NonGhostQuantifiers.dfy
diff --git a/Test/dafny0/ParallelResolveErrors.dfy b/Test/dafny0/ParallelResolveErrors.dfy
index 61956651..8c48487d 100644
--- a/Test/dafny0/ParallelResolveErrors.dfy
+++ b/Test/dafny0/ParallelResolveErrors.dfy
@@ -7,7 +7,6 @@ class C {
   ghost method Init_ModifyNothing() { }
   ghost method Init_ModifyThis() modifies this;
   {
-    data := 6;  // error: assignment to a non-ghost field
     gdata := 7;
   }
   ghost method Init_ModifyStuff(c: C) modifies this, c; { }
@@ -120,3 +119,15 @@ method M3(c: C)
     c.GhostMethodWithModifies(x);  // error: not allowed to call method with nonempty modifies clause
   }
 }
+
+module AnotherModule {
+  class C {
+    var data: int;
+    ghost var gdata: int;
+    ghost method Init_ModifyThis() modifies this;
+    {
+      data := 6;  // error: assignment to a non-ghost field
+      gdata := 7;
+    }
+  }
+}
diff --git a/Test/dafny0/ParallelResolveErrors.dfy.expect b/Test/dafny0/ParallelResolveErrors.dfy.expect
index 00030994..4d25ba11 100644
--- a/Test/dafny0/ParallelResolveErrors.dfy.expect
+++ b/Test/dafny0/ParallelResolveErrors.dfy.expect
@@ -1,23 +1,23 @@
-ParallelResolveErrors.dfy(10,9): 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)
-ParallelResolveErrors.dfy(21,4): Error: LHS of assignment must denote a mutable variable
-ParallelResolveErrors.dfy(26,6): Error: body of forall statement is attempting to update a variable declared outside the forall statement
+ParallelResolveErrors.dfy(129,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)
+ParallelResolveErrors.dfy(20,4): Error: LHS of assignment must denote a mutable variable
+ParallelResolveErrors.dfy(25,6): Error: body of forall statement is attempting to update a variable declared outside the forall statement
+ParallelResolveErrors.dfy(42,6): Error: body of forall statement is attempting to update a variable declared outside the forall statement
 ParallelResolveErrors.dfy(43,6): Error: body of forall statement is attempting to update a variable declared outside the forall statement
-ParallelResolveErrors.dfy(44,6): Error: body of forall statement is attempting to update a variable declared outside the forall statement
-ParallelResolveErrors.dfy(56,13): Error: new allocation not supported in forall statements
+ParallelResolveErrors.dfy(55,13): Error: new allocation not supported in forall statements
+ParallelResolveErrors.dfy(60,13): Error: new allocation not allowed in ghost context
 ParallelResolveErrors.dfy(61,13): Error: new allocation not allowed in ghost context
 ParallelResolveErrors.dfy(62,13): Error: new allocation not allowed in ghost context
 ParallelResolveErrors.dfy(63,13): Error: new allocation not allowed in ghost context
-ParallelResolveErrors.dfy(64,13): Error: new allocation not allowed in ghost context
-ParallelResolveErrors.dfy(65,22): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause
-ParallelResolveErrors.dfy(66,20): Error: the body of the enclosing forall statement is not allowed to call non-ghost methods
-ParallelResolveErrors.dfy(73,19): Error: trying to break out of more loop levels than there are enclosing loops
-ParallelResolveErrors.dfy(77,18): Error: return statement is not allowed inside a forall statement
-ParallelResolveErrors.dfy(84,21): Error: trying to break out of more loop levels than there are enclosing loops
-ParallelResolveErrors.dfy(85,20): Error: trying to break out of more loop levels than there are enclosing loops
-ParallelResolveErrors.dfy(86,20): Error: break label is undefined or not in scope: OutsideLoop
-ParallelResolveErrors.dfy(95,24): Error: trying to break out of more loop levels than there are enclosing loops
-ParallelResolveErrors.dfy(96,24): Error: break label is undefined or not in scope: OutsideLoop
-ParallelResolveErrors.dfy(107,9): Error: the body of the enclosing forall statement is not allowed to update heap locations
-ParallelResolveErrors.dfy(115,29): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause
-ParallelResolveErrors.dfy(120,29): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause
+ParallelResolveErrors.dfy(64,22): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause
+ParallelResolveErrors.dfy(65,20): Error: the body of the enclosing forall statement is not allowed to call non-ghost methods
+ParallelResolveErrors.dfy(72,19): Error: trying to break out of more loop levels than there are enclosing loops
+ParallelResolveErrors.dfy(76,18): Error: return statement is not allowed inside a forall statement
+ParallelResolveErrors.dfy(83,21): Error: trying to break out of more loop levels than there are enclosing loops
+ParallelResolveErrors.dfy(84,20): Error: trying to break out of more loop levels than there are enclosing loops
+ParallelResolveErrors.dfy(85,20): Error: break label is undefined or not in scope: OutsideLoop
+ParallelResolveErrors.dfy(94,24): Error: trying to break out of more loop levels than there are enclosing loops
+ParallelResolveErrors.dfy(95,24): Error: break label is undefined or not in scope: OutsideLoop
+ParallelResolveErrors.dfy(106,9): Error: the body of the enclosing forall statement is not allowed to update heap locations
+ParallelResolveErrors.dfy(114,29): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause
+ParallelResolveErrors.dfy(119,29): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause
 22 resolution/type errors detected in ParallelResolveErrors.dfy
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 2fab6bf3..d3514b2b 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -102,7 +102,7 @@ class EE {
 }
 
 // --------------- ghost tests -------------------------------------
-
+module HereAreMoreGhostTests {
 datatype GhostDt =
   Nil(ghost extraInfo: int) |
   Cons(data: int, tail: GhostDt, ghost moreInfo: int)
@@ -154,7 +154,7 @@ class GhostTests {
     ensures false;
   {
     while (true)
-      decreases *;  // error:  not allowed in ghost context
+//KRML-confirmed      decreases *;  // error:  not allowed in ghost context
     {
     }
   }
@@ -228,7 +228,7 @@ class GhostTests {
           if (p == 67) {
             break break;  // fine, since this is not a ghost context
           } else if (*) {
-            break break break;  // error: tries to break out of more loop levels than there are
+//KRML-confirmed            break break break;  // error: tries to break out of more loop levels than there are
           }
           q := q + 1;
         }
@@ -238,7 +238,7 @@ class GhostTests {
       p := p + 1;
     }
   }
-method BreakMayNotBeFineHere_Ghost(ghost t: int)
+  method BreakMayNotBeFineHere_Ghost(ghost t: int)
   {
     var n := 0;
     ghost var k := 0;
@@ -297,7 +297,7 @@ method BreakMayNotBeFineHere_Ghost(ghost t: int)
     }
   }
 }
-
+} //HereAreMoreGhostTests
 method DuplicateLabels(n: int) {
   var x;
   if (n < 7) {
@@ -364,17 +364,17 @@ method DatatypeDestructors(d: DTD_List) {
   }
 }
 method DatatypeDestructors_Ghost(d: DTD_List) {
-  var g1 := d.g;  // error: cannot use ghost member in non-ghost code
+  var g1 := d.g;  // error: cannot use ghost member in non-ghost code//KRML-confirmed
 }
 
 // ------------------- print statements ---------------------------------------
-
+module GhostPrintAttempts {
 method PrintOnlyNonGhosts(a: int, ghost b: int)
 {
   print "a: ", a, "\n";
   print "b: ", b, "\n";  // error: print statement cannot take ghosts
 }
-
+}
 // ------------------- auto-added type arguments ------------------------------
 
 class GenericClass<T> { var data: T; }
@@ -439,11 +439,11 @@ method TestCalc_Ghost(m: int, n: int, a: bool, b: bool)
 {
   calc {
     n + m;
-    { print n + m; } // error: non-ghost statements are not allowed in hints
+    { print n + m; } // error: non-ghost statements are not allowed in hints//KRML-confirmed
     m + n;
   }
 }
-
+module MyOwnModule {
 class SideEffectChecks {
   ghost var ycalc: int;
 
@@ -461,11 +461,11 @@ class SideEffectChecks {
     var x: int;
     calc {
       0;
-      { Mod(0); }     // methods with side-effects are not allowed
+      { Mod(0); }     // error: methods with side-effects are not allowed
       ycalc;
-      { ycalc := 1; } // heap updates are not allowed
+      { ycalc := 1; } // error: heap updates are not allowed
       1;
-      { x := 1; }     // updates to locals defined outside of the hint are not allowed
+      { x := 1; }     // error: updates to locals defined outside of the hint are not allowed
       x;
       {
         var x: int;
@@ -475,7 +475,7 @@ class SideEffectChecks {
     }
   }
 }
-
+}
 // ------------------- nameless constructors ------------------------------
 
 class YHWH {
@@ -523,13 +523,13 @@ method AssignSuchThatFromGhost()
   var x: int;
   ghost var g: int;
 
-  x := g;  // error: ghost cannot flow into non-ghost
+  x := g;  // error: ghost cannot flow into non-ghost//KRML-confirmed
 
   x := *;
   assume x == g;  // this mix of ghosts and non-ghosts is cool (but, of course,
                   // the compiler will complain)
 
-  x :| x == g;  // error: left-side has non-ghost, so RHS must be non-ghost as well
+  x :| x == g;  // error: left-side has non-ghost, so RHS must be non-ghost as well//KRML-confirmed
 
   x :| assume x == g;  // this is cool, since it's an assume (but, of course, the
                        // compiler will complain)
@@ -605,7 +605,7 @@ method LetSuchThat(ghost z: int, n: nat)
 }
 method LetSuchThat_Ghost(ghost z: int, n: nat)
 {
-  var x := var y :| y < z; y;  // error: contraint depend on ghost (z)
+  var x := var y :| y < z; y;  // error: contraint depend on ghost (z)//KRML-confirmed
 }
 
 // ------------ quantified variables whose types are not inferred ----------
@@ -677,9 +677,9 @@ module GhostAllocationTests {
       5;
       { var y := new G; }  // error: 'new' not allowed in ghost contexts
       2 + 3;
-      { if n != 0 { GhostNew4(n-1); } }  // error: cannot call non-ghost method in a ghost context
+      { if n != 0 { GhostNew4(n-1); } }  // error: cannot call non-ghost method in a ghost context//KRML-confirmed
       1 + 4;
-      { GhostNew5(g); }  // error: cannot call method with nonempty modifies
+      { GhostNew5(g); }  // error: cannot call method with nonempty modifies//KRML-confirmed
       -5 + 10;
     }
   }
@@ -735,7 +735,7 @@ module StatementsInExpressions {
     {
       calc {
         5;
-        { SideEffect(); }  // error: cannot call method with side effects
+        { SideEffect(); }  // error: cannot call method with side effects//KRML
         5;
       }
     }
@@ -745,7 +745,7 @@ module StatementsInExpressions {
       calc {
         6;
         { assert 6 < 8; }
-        { NonGhostMethod(); }  // error: cannot call non-ghost method
+        { NonGhostMethod(); }  // error: cannot call non-ghost method//KRML-confirmed
         { var x := 8;
           while x != 0
             decreases *;  // error: cannot use 'decreases *' in a ghost context
@@ -759,12 +759,12 @@ module StatementsInExpressions {
             x := x - 1;
           }
         }
-        { MyField := 12; }  // error: cannot assign to a field
-        { MyGhostField := 12; }  // error: cannot assign to any field
-        { SideEffect(); }  // error: cannot call (ghost) method with a modifies clause
+        { MyField := 12; }  // error: cannot assign to a field//KRML-confirmed
+        { MyGhostField := 12; }  // error: cannot assign to any field//KRML-confirmed
+        { SideEffect(); }  // error: cannot call (ghost) method with a modifies clause//KRML-confirmed
         { var x := 8;
           while x != 0
-            modifies this;  // error: cannot use a modifies clause on a loop
+            modifies this;  // error: cannot use a modifies clause on a loop//KRML-confirmed
           {
             x := x - 1;
           }
@@ -783,7 +783,7 @@ module StatementsInExpressions {
       calc {
         6;
         { assert 6 < 8; }
-        { NonGhostMethod(); }  // error: cannot call non-ghost method
+        { NonGhostMethod(); }  // error: cannot call non-ghost method//KRML-confirmed
         { var x := 8;
           while x != 0
             decreases *;  // error: cannot use 'decreases *' in a ghost context
@@ -791,12 +791,12 @@ module StatementsInExpressions {
             x := x - 1;
           }
         }
-        { MyField := 12; }  // error: cannot assign to a field
-        { MyGhostField := 12; }  // error: cannot assign to any field
-        { M(); }  // error: cannot call (ghost) method with a modifies clause
+        { MyField := 12; }  // error: cannot assign to a field//KRML-confirmed
+        { MyGhostField := 12; }  // error: cannot assign to any field//KRML-confirmed
+        { M(); }  // error: cannot call (ghost) method with a modifies clause//KRML-confirmed
         { var x := 8;
           while x != 0
-            modifies this;  // error: cannot use a modifies clause on a loop
+            modifies this;  // error: cannot use a modifies clause on a loop//KRML-confirmed
           {
             x := x - 1;
           }
@@ -822,7 +822,7 @@ module StatementsInExpressions {
     {
       MyLemma();
       MyGhostMethod();   // error: modifi2es state
-      OrdinaryMethod();  // error: not a ghost
+      OrdinaryMethod();  // error: not a ghost//KRML-confirmed
       OutParamMethod();  // error: has out-parameters
       10
     }
@@ -1446,3 +1446,219 @@ module SuchThat {
     w
   }
 }
+
+// ---------------------- NEW STUFF ----------------------------------------
+
+module GhostTests {
+  class G { }
+  
+  method GhostNew4(n: nat)
+  {
+    var g := new G;
+    calc {
+      5;
+      2 + 3;
+      { if n != 0 { GhostNew4(n-1); } }  // error: cannot call non-ghost method in a ghost context//ADD:680
+      1 + 4;
+      { GhostNew5(g); }  // error: cannot call method with nonempty modifies//ADD:682
+      -5 + 10;
+    }
+  }
+
+  ghost method GhostNew5(g: G)
+    modifies g;
+  {
+  }
+  
+  class MyClass {
+    ghost method SideEffect()
+      modifies this;
+    {
+    }
+
+    method NonGhostMethod()
+    {
+    }
+
+    ghost method M()
+      modifies this;
+    {
+      calc {
+        5;
+        { SideEffect(); }  // error: cannot call method with side effects//ADD:738
+        5;
+      }
+    }
+    function F(): int
+    {
+      calc {
+        6;
+        { assert 6 < 8; }
+        { NonGhostMethod(); }  // error: cannot call non-ghost method//ADD:748
+        { var x := 8;
+          while x != 0
+          {
+            x := x - 1;
+          }
+        }
+        { var x := 8;
+          while x != 0
+          {
+            x := x - 1;
+          }
+        }
+        { MyField := 12; }  // error: cannot assign to a field, and especially not a non-ghost field//ADD:762
+        { MyGhostField := 12; }  // error: cannot assign to any field//ADD:763
+        { SideEffect(); }  // error: cannot call (ghost) method with a modifies clause//ADD:764
+        { var x := 8;
+          while x != 0
+            modifies this;  // error: cannot use a modifies clause on a loop//ADD:767
+          {
+            x := x - 1;
+          }
+        }
+        6;
+      }
+      5
+    }
+    var MyField: int;
+    ghost var MyGhostField: int;
+    method N()
+    {
+      var y :=
+      calc {
+        6;
+        { assert 6 < 8; }
+        { NonGhostMethod(); }  // error: cannot call non-ghost method//ADD:786
+        { var x := 8;
+          while x != 0
+          {
+            x := x - 1;
+          }
+        }
+        { MyField := 12; }  // error: cannot assign to a field, and especially not a non-ghost field//ADD:794
+        { MyGhostField := 12; }  // error: cannot assign to any field//ADD:795
+        { M(); }  // error: cannot call (ghost) method with a modifies clause//ADD:796
+        { var x := 8;
+          while x != 0
+            modifies this;  // error: cannot use a modifies clause on a loop//ADD:799
+          {
+            x := x - 1;
+          }
+        }
+        { var x := 8;
+          while x != 0
+          {
+            x := x - 1;
+          }
+        }
+        6;
+      }
+      5;
+    }
+    ghost method MyLemma()
+    ghost method MyGhostMethod()
+      modifies this;
+    method OrdinaryMethod()
+    ghost method OutParamMethod() returns (y: int)
+
+    function UseLemma(): int
+    {
+      MyLemma();
+      OrdinaryMethod();  // error: not a ghost//ADD:825
+      10
+    }
+  }
+}
+
+module EvenMoreGhostTests {
+  ghost method NiceTry()
+    ensures false;
+  {
+    while (true)
+      decreases *;  // error:  not allowed in ghost context//ADD:157
+    {
+    }
+  }
+  method BreakMayNotBeFineHere()
+  {
+    var n := 0;
+    var p := 0;
+    while (true)
+    {
+      var dontKnow;
+      if (n == 112) {
+      } else if (dontKnow == 708) {
+        while * {
+          label IfNest:
+          if (p == 67) {
+            break break;  // fine, since this is not a ghost context
+          } else if (*) {
+            break break break;  // error: tries to break out of more loop levels than there are//ADD:231
+          }
+        }
+      }
+    }
+  }
+  ghost method Bad()
+  {
+    var x: int;
+    calc {
+      1;
+//******      { x := 1; }     // error: updates to locals defined outside of the hint are not allowed
+      x;
+      {
+        var x: int;
+        x := 1;       // this is OK
+      }
+      1;
+    }
+  }
+}
+
+module BadGhostTransfer {
+  datatype DTD_List = DTD_Nil | DTD_Cons(Car: int, Cdr: DTD_List, ghost g: int)
+
+  method DatatypeDestructors_Ghost(d: DTD_List) {
+    var g1 := d.g;  // error: cannot use ghost member in non-ghost code//ADD:367
+  }
+  method AssignSuchThatFromGhost()
+  {
+    var x: int;
+    ghost var g: int;
+
+    x := g;  // error: ghost cannot flow into non-ghost//ADD:526
+
+    x := *;
+    assume x == g;  // this mix of ghosts and non-ghosts is cool (but, of course,
+                    // the compiler will complain)
+
+    x :| x == g;  // error: left-side has non-ghost, so RHS must be non-ghost as well//ADD:532
+
+    x :| assume x == g;  // this is cool, since it's an assume (but, of course, the
+                         // compiler will complain)
+
+    x :| x == 5;
+    g :| g <= g;
+    g :| assume g < g;  // the compiler will complain here, despite the LHS being
+                        // ghost -- and rightly so, since an assume is used
+  }
+}
+
+module MoreGhostPrintAttempts {
+  method TestCalc_Ghost(m: int, n: int, a: bool, b: bool)
+  {
+    calc {
+      n + m;
+      { print n + m; } // error: non-ghost statements are not allowed in hints//ADD:442
+      m + n;
+    }
+  }
+}
+
+module MoreLetSuchThatExpr {
+  method LetSuchThat_Ghost(ghost z: int, n: nat)
+  {
+    var x := var y :| y < z; y;  // error: contraint depend on ghost (z)//ADD:608
+  }
+}
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
diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy
index b44f4d68..a9d473f6 100644
--- a/Test/dafny0/TypeTests.dfy
+++ b/Test/dafny0/TypeTests.dfy
@@ -39,7 +39,7 @@ datatype ReverseOrder_TheCounterpart<T> =
 
 // ---------------------
 
-class ArrayTests {
+module ArrayTests {
   ghost method G(a: array<int>)
     requires a != null && 10 <= a.Length;
     modifies a;
@@ -167,31 +167,33 @@ module Expl_Module {
 
 // --------------------- more ghost tests, for assign-such-that statements
 
-method M()
-{
-  ghost var b: bool;
-  ghost var k: int, l: int;
-  var m: int;
-
-  k :| k < 10;
-  k, m :| 0 <= k < m;  // error: LHS has non-ghost and RHS has ghost
-  m :| m < 10;
-
-  // Because of the ghost guard, these 'if' statements are ghost contexts, so only
-  // assignments to ghosts are allowed.
-  if (b) {
-    k :| k < 10;  // should be allowed
-    k, l :| 0 <= k < l;  // ditto
-  }
-  if (b) {
-    m :| m < 10;  // error: not allowed in ghost context
-    k, m :| 0 <= k < m;  // error: not allowed in ghost context
+module MoreGhostTests {
+  method M()
+  {
+    ghost var b: bool;
+    ghost var k: int, l: int;
+    var m: int;
+
+    k :| k < 10;
+    k, m :| 0 <= k < m;  // error: LHS has non-ghost and RHS has ghost
+    m :| m < 10;
+
+    // Because of the ghost guard, these 'if' statements are ghost contexts, so only
+    // assignments to ghosts are allowed.
+    if (b) {
+      k :| k < 10;  // should be allowed
+      k, l :| 0 <= k < l;  // ditto
+    }
+    if (b) {
+      m :| m < 10;  // error: not allowed in ghost context
+      k, m :| 0 <= k < m;  // error: not allowed in ghost context
+    }
   }
-}
 
-ghost method GhostM() returns (x: int)
-{
-  x :| true;  // no problem (but there once was a problem with this case, where an error was generated for no reason)
+  ghost method GhostM() returns (x: int)
+  {
+    x :| true;  // no problem (but there once was a problem with this case, where an error was generated for no reason)
+  }
 }
 
 // ------------------ cycles that could arise from proxy assignments ---------
diff --git a/Test/dafny0/TypeTests.dfy.expect b/Test/dafny0/TypeTests.dfy.expect
index 8206fd43..de0bfbed 100644
--- a/Test/dafny0/TypeTests.dfy.expect
+++ b/Test/dafny0/TypeTests.dfy.expect
@@ -1,6 +1,10 @@
-TypeTests.dfy(205,15): Error: incorrect type of datatype constructor argument (found ? -> ?, expected ? -> Dt<?>)
-TypeTests.dfy(211,15): Error: incorrect type of datatype constructor argument (found ? -> ?, expected ? -> Dt<?>)
-TypeTests.dfy(218,6): Error: RHS (of type set<?>) not assignable to LHS (of type ?)
+TypeTests.dfy(47,9): Error: Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
+TypeTests.dfy(178,7): Error: non-ghost variable cannot be assigned a value that depends on a ghost
+TypeTests.dfy(188,6): Error: cannot assign to non-ghost variable in a ghost context
+TypeTests.dfy(189,9): Error: cannot assign to non-ghost variable in a ghost context
+TypeTests.dfy(207,15): Error: incorrect type of datatype constructor argument (found ? -> ?, expected ? -> Dt<?>)
+TypeTests.dfy(213,15): Error: incorrect type of datatype constructor argument (found ? -> ?, expected ? -> Dt<?>)
+TypeTests.dfy(220,6): Error: RHS (of type set<?>) not assignable to LHS (of type ?)
 TypeTests.dfy(7,17): Error: type mismatch for argument 0 (function expects C, got D)
 TypeTests.dfy(7,20): Error: type mismatch for argument 1 (function expects D, got C)
 TypeTests.dfy(8,15): Error: type mismatch for argument 0 (function expects C, got int)
@@ -8,7 +12,6 @@ TypeTests.dfy(8,18): Error: type mismatch for argument 1 (function expects D, go
 TypeTests.dfy(14,16): Error: incorrect type of method in-parameter 0 (expected int, got bool)
 TypeTests.dfy(15,12): Error: incorrect type of method out-parameter 0 (expected int, got C)
 TypeTests.dfy(15,12): Error: incorrect type of method out-parameter 1 (expected C, got int)
-TypeTests.dfy(47,9): Error: Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
 TypeTests.dfy(56,6): Error: Duplicate local-variable name: z
 TypeTests.dfy(58,6): Error: Duplicate local-variable name: x
 TypeTests.dfy(61,8): Error: Duplicate local-variable name: x
@@ -56,8 +59,5 @@ TypeTests.dfy(151,13): Error: sorry, cannot instantiate type parameter with a su
 TypeTests.dfy(152,2): Error: sorry, cannot instantiate type parameter with a subrange type
 TypeTests.dfy(153,16): Error: sorry, cannot instantiate type parameter with a subrange type
 TypeTests.dfy(154,14): Error: sorry, cannot instantiate type parameter with a subrange type
-TypeTests.dfy(177,5): Error: non-ghost variable cannot be assigned a value that depends on a ghost
-TypeTests.dfy(187,4): Error: cannot assign to non-ghost variable in a ghost context
-TypeTests.dfy(188,7): Error: cannot assign to non-ghost variable in a ghost context
 TypeTests.dfy(21,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed
 62 resolution/type errors detected in TypeTests.dfy
diff --git a/Test/dafny4/set-compr.dfy.expect b/Test/dafny4/set-compr.dfy.expect
index b31c6ac0..615ee2bc 100644
--- a/Test/dafny4/set-compr.dfy.expect
+++ b/Test/dafny4/set-compr.dfy.expect
@@ -1,3 +1,3 @@
-set-compr.dfy(25,7): 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'
-set-compr.dfy(51,13): 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'
+set-compr.dfy(25,7): 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'
+set-compr.dfy(51,13): 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'
 2 resolution/type errors detected in set-compr.dfy
author	leino <unknown>	2015-09-28 13:16:15 -0700
committer	leino <unknown>	2015-09-28 13:16:15 -0700
commit	0c1ec594e68dab4fcd458a00f9f7a1ac6de2e218 (patch)
tree	cb89d6ef66c96bfa171f954898548f295a3cabc0
parent	ebaaa36321463925dc9030455e87ae17732b2353 (diff)