Disallow allocations in ghost contexts

9 files changed, 372 insertions, 188 deletions

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 7b932078..561a29a1 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -520,12 +520,14 @@ axiom (forall<T> cl : ClassName, nm: NameFamily ::
    {FieldOfDecl(cl, nm): Field T}

    DeclType(FieldOfDecl(cl, nm): Field T) == cl && DeclName(FieldOfDecl(cl, nm): Field T) == nm);

 

+function $IsGhostField<T>(Field T): bool;

+

 // ---------------------------------------------------------------

 // -- Allocatedness ----------------------------------------------

 // ---------------------------------------------------------------

 

 const unique alloc: Field bool;

-axiom FDim(alloc) == 0;

+axiom FDim(alloc) == 0 && !$IsGhostField(alloc);  // treat as non-ghost field, because it cannot be changed by ghost code

 

 function DtAlloc(DatatypeType, HeapType): bool;

 axiom (forall h, k: HeapType, d: DatatypeType ::

@@ -611,6 +613,13 @@ axiom (forall a,b,c: HeapType :: { $HeapSucc(a,b), $HeapSucc(b,c) }
 axiom (forall h: HeapType, k: HeapType :: { $HeapSucc(h,k) }

   $HeapSucc(h,k) ==> (forall o: ref :: { read(k, o, alloc) } read(h, o, alloc) ==> read(k, o, alloc)));

 

+function $HeapSuccGhost(HeapType, HeapType): bool;

+axiom (forall h: HeapType, k: HeapType :: { $HeapSuccGhost(h,k) }

+  $HeapSuccGhost(h,k) ==>

+    $HeapSucc(h,k) &&

+    (forall<alpha> o: ref, f: Field alpha :: { read(k, o, f) }

+      !$IsGhostField(f) ==> read(h, o, f) == read(k, o, f)));

+

 // ---------------------------------------------------------------

 // -- Useful macros ----------------------------------------------

 // ---------------------------------------------------------------

diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 0250b2a3..265dd3ea 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/Dafny/Resolver.cs
@@ -4417,10 +4417,7 @@ namespace Microsoft.Dafny
           if (kind == ForallStmt.ParBodyKind.Assign) {

             Error(rhs.Tok, "new allocation not supported in forall statements");

           } else {

-            var t = (TypeRhs)rhs;

-            if (t.InitCall != null) {

-              CheckForallStatementBodyRestrictions(t.InitCall, kind);

-            }

+            Error(rhs.Tok, "new allocation not allowed in ghost context");

           }

         } else if (rhs is ExprRhs) {

           var r = ((ExprRhs)rhs).Expr.Resolved;

@@ -4442,6 +4439,9 @@ namespace Microsoft.Dafny
             Error(stmt, "the body of the enclosing forall statement is not allowed to update heap locations");

           }

         }

+        if (s.Method.Mod.Expressions.Count != 0) {

+          Error(stmt, "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");

+        }

         if (!s.Method.IsGhost) {

           // The reason for this restriction is that the compiler is going to omit the forall statement altogether--it has

           // no effect.  However, print effects are not documented, so to make sure that the compiler does not omit a call to

@@ -4652,6 +4652,10 @@ namespace Microsoft.Dafny
       Contract.Requires(codeContext != null);

       Contract.Ensures(Contract.Result<Type>() != null);

 

+      // "new" is not allowed in ghost contexts

+      if (specContextOnly) {

+        Error(rr.Tok, "'new' is not allowed in ghost contexts");

+      }

       if (rr.Type == null) {

         if (rr.ArrayDimensions != null) {

           // ---------- new T[EE]

diff --git a/Source/Dafny/Rewriter.cs b/Source/Dafny/Rewriter.cs
index f248fae2..c5351589 100644
--- a/Source/Dafny/Rewriter.cs
+++ b/Source/Dafny/Rewriter.cs
@@ -315,7 +315,7 @@ namespace Microsoft.Dafny
       // A simple query method has out parameters, its body has no effect other than to assign to them,

       // and the postcondition does not explicitly mention the pre-state.

       return m.Outs.Count != 0 && m.Body != null && LocalAssignsOnly(m.Body) &&

-        m.Ens.TrueForAll(mfe => !Translator.MentionsOldState(mfe.E));

+        m.Ens.TrueForAll(mfe => !MentionsOldState(mfe.E));

     }

 

     bool LocalAssignsOnly(Statement s) {

@@ -338,6 +338,22 @@ namespace Microsoft.Dafny
       return true;

     }

 

+    /// <summary>

+    /// Returns true iff 'expr' is a two-state expression, that is, if it mentions "old(...)" or "fresh(...)".

+    /// </summary>

+    static bool MentionsOldState(Expression expr) {

+      Contract.Requires(expr != null);

+      if (expr is OldExpr || expr is FreshExpr) {

+        return true;

+      }

+      foreach (var ee in expr.SubExpressions) {

+        if (MentionsOldState(ee)) {

+          return true;

+        }

+      }

+      return false;

+    }

+

     public static BinaryExpr BinBoolExpr(Boogie.IToken tok, BinaryExpr.ResolvedOpcode rop, Expression e0, Expression e1) {

       var p = new BinaryExpr(tok, BinaryExpr.ResolvedOp2SyntacticOp(rop), e0, e1);

       p.ResolvedOp = rop;  // resolve here

diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 0fef4319..03cee979 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -1085,7 +1085,7 @@ namespace Microsoft.Dafny {
           }

           comment = null;

         }

-        foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(iter.tok, iter.Modifies.Expressions, etran.Old, etran, etran.Old)) {

+        foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(iter.tok, iter.Modifies.Expressions, false, etran.Old, etran, etran.Old)) {

           ens.Add(Ensures(tri.tok, tri.IsFree, tri.Expr, tri.ErrorMessage, tri.Comment));

         }

       }

@@ -2080,7 +2080,7 @@ namespace Microsoft.Dafny {
         // play havoc with the heap according to the modifies clause

         builder.Add(new Bpl.HavocCmd(m.tok, new Bpl.IdentifierExprSeq((Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)etran.HeapExpr)));

         // assume the usual two-state boilerplate information

-        foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(m.tok, m.Mod.Expressions, etran.Old, etran, etran.Old))

+        foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(m.tok, m.Mod.Expressions, m.IsGhost, etran.Old, etran, etran.Old))

         {

           if (tri.IsFree) {

             builder.Add(new Bpl.AssumeCmd(m.tok, tri.Expr));

@@ -3682,10 +3682,16 @@ namespace Microsoft.Dafny {
         Bpl.Type ty = predef.FieldName(f.tok, TrType(f.Type));

         fc = new Bpl.Constant(f.tok, new Bpl.TypedIdent(f.tok, f.FullCompileName, ty), false);

         fields.Add(f, fc);

-        // axiom FDim(f) == 0 && FieldOfDecl(C, name) == f;

+        // axiom FDim(f) == 0 && FieldOfDecl(C, name) == f &&

+        //       $IsGhostField(f);    // if the field is a ghost field

+        // OR:

+        //       !$IsGhostField(f);    // if the field is not a ghost field

         Bpl.Expr fdim = Bpl.Expr.Eq(FunctionCall(f.tok, BuiltinFunction.FDim, ty, Bpl.Expr.Ident(fc)), Bpl.Expr.Literal(0));

         Bpl.Expr declType = Bpl.Expr.Eq(FunctionCall(f.tok, BuiltinFunction.FieldOfDecl, ty, new Bpl.IdentifierExpr(f.tok, GetClass(cce.NonNull(f.EnclosingClass))), new Bpl.IdentifierExpr(f.tok, GetFieldNameFamily(f.Name))), Bpl.Expr.Ident(fc));

-        Bpl.Axiom ax = new Bpl.Axiom(f.tok, Bpl.Expr.And(fdim, declType));

+        Bpl.Expr cond = Bpl.Expr.And(fdim, declType);

+        var ig = FunctionCall(f.tok, BuiltinFunction.IsGhostField, ty, Bpl.Expr.Ident(fc));

+        cond = Bpl.Expr.And(cond, f.IsGhost ? ig : Bpl.Expr.Not(ig));

+        Bpl.Axiom ax = new Bpl.Axiom(f.tok, cond);

         sink.TopLevelDeclarations.Add(ax);

       }

       return fc;

@@ -3868,7 +3874,7 @@ namespace Microsoft.Dafny {
           }

           comment = null;

         }

-        foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(m.tok, m.Mod.Expressions, etran.Old, etran, etran.Old)) {

+        foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(m.tok, m.Mod.Expressions, m.IsGhost, etran.Old, etran, etran.Old)) {

           ens.Add(Ensures(tri.tok, tri.IsFree, tri.Expr, tri.ErrorMessage, tri.Comment));

         }

       }

@@ -3944,7 +3950,7 @@ namespace Microsoft.Dafny {
           ens.Add(Ensures(s.E.tok, s.IsOnlyFree, s.E, "Error: postcondition of refined method may be violated", null));

         }

       }

-      foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(m.tok, m.Mod.Expressions, etran.Old, etran, etran.Old)) {

+      foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(m.tok, m.Mod.Expressions, m.IsGhost, etran.Old, etran, etran.Old)) {

         ens.Add(Ensures(tri.tok, tri.IsFree, tri.Expr, tri.ErrorMessage, tri.Comment));

       }

 

@@ -4237,7 +4243,7 @@ namespace Microsoft.Dafny {
     ///  S2. the post-state of the two-state interval

     /// This method assumes that etranPre denotes S1, etran denotes S2, and that etranMod denotes S0.

     /// </summary>

-    List<BoilerplateTriple/*!*/>/*!*/ GetTwoStateBoilerplate(IToken/*!*/ tok, List<FrameExpression/*!*/>/*!*/ modifiesClause, ExpressionTranslator/*!*/ etranPre, ExpressionTranslator/*!*/ etran, ExpressionTranslator/*!*/ etranMod)

+    List<BoilerplateTriple/*!*/>/*!*/ GetTwoStateBoilerplate(IToken/*!*/ tok, List<FrameExpression/*!*/>/*!*/ modifiesClause, bool isGhostContext, ExpressionTranslator/*!*/ etranPre, ExpressionTranslator/*!*/ etran, ExpressionTranslator/*!*/ etranMod)

     {

       Contract.Requires(tok != null);

       Contract.Requires(modifiesClause != null);

@@ -4245,15 +4251,17 @@ namespace Microsoft.Dafny {
       Contract.Requires(etran != null);

       Contract.Ensures(cce.NonNullElements(Contract.Result<List<BoilerplateTriple>>()));

 

-      List<BoilerplateTriple> boilerplate = new List<BoilerplateTriple>();

-

-      // the frame condition, which is free since it is checked with every heap update and call

-      boilerplate.Add(new BoilerplateTriple(tok, true, FrameCondition(tok, modifiesClause, etranPre, etran, etranMod), null, "frame condition"));

-

-      // HeapSucc(S1, S2)

-      Bpl.Expr heapSucc = FunctionCall(tok, BuiltinFunction.HeapSucc, null, etranPre.HeapExpr, etran.HeapExpr);

-      boilerplate.Add(new BoilerplateTriple(tok, true, heapSucc, null, "boilerplate"));

-

+      var boilerplate = new List<BoilerplateTriple>();

+      if (isGhostContext && modifiesClause.Count == 0) {

+        // plain and simple:  S1 == S2

+        boilerplate.Add(new BoilerplateTriple(tok, true, Bpl.Expr.Eq(etranPre.HeapExpr, etran.HeapExpr), null, "frame condition"));

+      } else {

+        // the frame condition, which is free since it is checked with every heap update and call

+        boilerplate.Add(new BoilerplateTriple(tok, true, FrameCondition(tok, modifiesClause, isGhostContext, etranPre, etran, etranMod), null, "frame condition"));

+        // HeapSucc(S1, S2) or HeapSuccGhost(S1, S2)

+        Bpl.Expr heapSucc = FunctionCall(tok, isGhostContext ? BuiltinFunction.HeapSuccGhost : BuiltinFunction.HeapSucc, null, etranPre.HeapExpr, etran.HeapExpr);

+        boilerplate.Add(new BoilerplateTriple(tok, true, heapSucc, null, "boilerplate"));

+      }

       return boilerplate;

     }

 

@@ -4264,7 +4272,7 @@ namespace Microsoft.Dafny {
     ///  S2. the post-state of the two-state interval

     /// This method assumes that etranPre denotes S1, etran denotes S2, and that etranMod denotes S0.

     /// </summary>

-    Bpl.Expr/*!*/ FrameCondition(IToken/*!*/ tok, List<FrameExpression/*!*/>/*!*/ modifiesClause, ExpressionTranslator/*!*/ etranPre, ExpressionTranslator/*!*/ etran, ExpressionTranslator/*!*/ etranMod)

+    Bpl.Expr/*!*/ FrameCondition(IToken/*!*/ tok, List<FrameExpression/*!*/>/*!*/ modifiesClause, bool isGhostContext, ExpressionTranslator/*!*/ etranPre, ExpressionTranslator/*!*/ etran, ExpressionTranslator/*!*/ etranMod)

     {

       Contract.Requires(tok != null);

       Contract.Requires(etran != null);

@@ -4275,23 +4283,28 @@ namespace Microsoft.Dafny {
 

       // generate:

       //  (forall<alpha> o: ref, f: Field alpha :: { $Heap[o,f] }

-      //      o != null && old($Heap)[o,alloc] ==>

+      //      o != null

+      //      && old($Heap)[o,alloc]                     // include only in non-ghost contexts

+      //      ==>

       //        $Heap[o,f] == PreHeap[o,f] ||

       //        (o,f) in modifiesClause)

-      Bpl.TypeVariable alpha = new Bpl.TypeVariable(tok, "alpha");

-      Bpl.BoundVariable oVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$o", predef.RefType));

-      Bpl.IdentifierExpr o = new Bpl.IdentifierExpr(tok, oVar);

-      Bpl.BoundVariable fVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$f", predef.FieldName(tok, alpha)));

-      Bpl.IdentifierExpr f = new Bpl.IdentifierExpr(tok, fVar);

+      var alpha = new Bpl.TypeVariable(tok, "alpha");

+      var oVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$o", predef.RefType));

+      var o = new Bpl.IdentifierExpr(tok, oVar);

+      var fVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$f", predef.FieldName(tok, alpha)));

+      var f = new Bpl.IdentifierExpr(tok, fVar);

 

       Bpl.Expr heapOF = ExpressionTranslator.ReadHeap(tok, etran.HeapExpr, o, f);

       Bpl.Expr preHeapOF = ExpressionTranslator.ReadHeap(tok, etranPre.HeapExpr, o, f);

-      Bpl.Expr ante = Bpl.Expr.And(Bpl.Expr.Neq(o, predef.Null), etranMod.IsAlloced(tok, o));

+      Bpl.Expr ante = Bpl.Expr.Neq(o, predef.Null);

+      if (!isGhostContext) {

+        ante = Bpl.Expr.And(ante, etranMod.IsAlloced(tok, o));

+      }

       Bpl.Expr consequent = Bpl.Expr.Eq(heapOF, preHeapOF);

 

       consequent = Bpl.Expr.Or(consequent, InRWClause(tok, o, f, modifiesClause, etranMod, null, null));

 

-      Bpl.Trigger tr = new Bpl.Trigger(tok, true, new Bpl.ExprSeq(heapOF));

+      var tr = new Bpl.Trigger(tok, true, new Bpl.ExprSeq(heapOF));

       return new Bpl.ForallExpr(tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fVar), null, tr, Bpl.Expr.Imp(ante, consequent));

     }

     Bpl.Expr/*!*/ FrameConditionUsingDefinedFrame(IToken/*!*/ tok, ExpressionTranslator/*!*/ etranPre, ExpressionTranslator/*!*/ etran, ExpressionTranslator/*!*/ etranMod)

@@ -4780,9 +4793,9 @@ namespace Microsoft.Dafny {
           builder, locals, etran);

 

       } else if (stmt is ForallStmt) {

-        AddComment(builder, stmt, "forall statement");

         var s = (ForallStmt)stmt;

         if (s.Kind == ForallStmt.ParBodyKind.Assign) {

+          AddComment(builder, stmt, "forall statement (assign)");

           Contract.Assert(s.Ens.Count == 0);

           if (s.BoundVars.Count == 0) {

             TrStmt(s.Body, builder, locals, etran);

@@ -4797,8 +4810,10 @@ namespace Microsoft.Dafny {
           }

 

         } else if (s.Kind == ForallStmt.ParBodyKind.Call) {

+          AddComment(builder, stmt, "forall statement (call)");

           Contract.Assert(s.Ens.Count == 0);

           if (s.BoundVars.Count == 0) {

+            Contract.Assert(LiteralExpr.IsTrue(s.Range));  // follows from the invariant of ForallStmt

             TrStmt(s.Body, builder, locals, etran);

           } else {

             var s0 = (CallStmt)s.S0;

@@ -4811,6 +4826,7 @@ namespace Microsoft.Dafny {
           }

 

         } else if (s.Kind == ForallStmt.ParBodyKind.Proof) {

+          AddComment(builder, stmt, "forall statement (proof)");

           var definedness = new Bpl.StmtListBuilder();

           var exporter = new Bpl.StmtListBuilder();

           TrForallProof(s, definedness, exporter, locals, etran);

@@ -5301,18 +5317,20 @@ namespace Microsoft.Dafny {
       // INIT is the substitution [old($Heap),$Heap := old($Heap),initHeap].

 

       if (definedness != null) {

-        // Note, it would be nicer (and arguably more appropriate) to do a SetupBoundVarsAsLocals

-        // here (rather than a TrBoundVariables).  However, there is currently no way to apply

-        // a substMap to a statement (in particular, to s.Body), so that doesn't work here.

-        Bpl.VariableSeq bvars = new Bpl.VariableSeq();

-        var ante = etran.TrBoundVariables(boundVars, bvars, true);

-        locals.AddRange(bvars);

-        var havocIds = new Bpl.IdentifierExprSeq();

-        foreach (Bpl.Variable bv in bvars) {

-          havocIds.Add(new Bpl.IdentifierExpr(tok, bv));

+        if (boundVars.Count != 0) {

+          // Note, it would be nicer (and arguably more appropriate) to do a SetupBoundVarsAsLocals

+          // here (rather than a TrBoundVariables).  However, there is currently no way to apply

+          // a substMap to a statement (in particular, to s.Body), so that doesn't work here.

+          Bpl.VariableSeq bvars = new Bpl.VariableSeq();

+          var ante = etran.TrBoundVariables(boundVars, bvars, true);

+          locals.AddRange(bvars);

+          var havocIds = new Bpl.IdentifierExprSeq();

+          foreach (Bpl.Variable bv in bvars) {

+            havocIds.Add(new Bpl.IdentifierExpr(tok, bv));

+          }

+          definedness.Add(new Bpl.HavocCmd(tok, havocIds));

+          definedness.Add(new Bpl.AssumeCmd(tok, ante));

         }

-        definedness.Add(new Bpl.HavocCmd(tok, havocIds));

-        definedness.Add(new Bpl.AssumeCmd(tok, ante));

         TrStmt_CheckWellformed(range, definedness, locals, etran, false);

         definedness.Add(new Bpl.AssumeCmd(range.tok, etran.TrExpr(range)));

         if (additionalRange != null) {

@@ -5334,22 +5352,18 @@ namespace Microsoft.Dafny {
         var initEtran = new ExpressionTranslator(this, predef, initHeap, etran.Old.HeapExpr);

         // initHeap := $Heap;

         exporter.Add(Bpl.Cmd.SimpleAssign(tok, initHeap, etran.HeapExpr));

-        if (s0.Method.Ens.Exists(ens => MentionsOldState(ens.E))) {

-          var heapIdExpr = (Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)etran.HeapExpr;

-          // advance $Heap, Tick;

-          exporter.Add(new Bpl.HavocCmd(tok, new Bpl.IdentifierExprSeq(heapIdExpr, etran.Tick())));

-          foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(tok, new List<FrameExpression>(), initEtran, etran, initEtran)) {

-            if (tri.IsFree) {

-              exporter.Add(new Bpl.AssumeCmd(tok, tri.Expr));

-            }

-          }

-          if (codeContext is IteratorDecl) {

-            var iter = (IteratorDecl)codeContext;

-            RecordNewObjectsIn_New(tok, iter, initHeap, heapIdExpr, exporter, locals, etran);

+        var heapIdExpr = (Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)etran.HeapExpr;

+        // advance $Heap, Tick;

+        exporter.Add(new Bpl.HavocCmd(tok, new Bpl.IdentifierExprSeq(heapIdExpr, etran.Tick())));

+        Contract.Assert(s0.Method.Mod.Expressions.Count == 0);  // checked by the resolver

+        foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(tok, new List<FrameExpression>(), s0.IsGhost, initEtran, etran, initEtran)) {

+          if (tri.IsFree) {

+            exporter.Add(new Bpl.AssumeCmd(tok, tri.Expr));

           }

-        } else {

-          // As an optimization, create the illusion that the $Heap is unchanged by the forall-statement body.

-          exporter.Add(new Bpl.HavocCmd(tok, new Bpl.IdentifierExprSeq(etran.Tick())));

+        }

+        if (codeContext is IteratorDecl) {

+          var iter = (IteratorDecl)codeContext;

+          RecordNewObjectsIn_New(tok, iter, initHeap, heapIdExpr, exporter, locals, etran);

         }

 

         var bvars = new Bpl.VariableSeq();

@@ -5433,18 +5447,20 @@ namespace Microsoft.Dafny {
       //     assume (forall x,y :: Range(x,y)[old($Heap),$Heap := old($Heap),initHeap] ==> Post(x,y));

       //   }

 

-      // Note, it would be nicer (and arguably more appropriate) to do a SetupBoundVarsAsLocals

-      // here (rather than a TrBoundVariables).  However, there is currently no way to apply

-      // a substMap to a statement (in particular, to s.Body), so that doesn't work here.

-      Bpl.VariableSeq bvars = new Bpl.VariableSeq();

-      var ante = etran.TrBoundVariables(s.BoundVars, bvars, true);

-      locals.AddRange(bvars);

-      var havocIds = new Bpl.IdentifierExprSeq();

-      foreach (Bpl.Variable bv in bvars) {

-        havocIds.Add(new Bpl.IdentifierExpr(s.Tok, bv));

-      }

-      definedness.Add(new Bpl.HavocCmd(s.Tok, havocIds));

-      definedness.Add(new Bpl.AssumeCmd(s.Tok, ante));

+      if (s.BoundVars.Count != 0) {

+        // Note, it would be nicer (and arguably more appropriate) to do a SetupBoundVarsAsLocals

+        // here (rather than a TrBoundVariables).  However, there is currently no way to apply

+        // a substMap to a statement (in particular, to s.Body), so that doesn't work here.

+        var bVars = new Bpl.VariableSeq();

+        var typeAntecedent = etran.TrBoundVariables(s.BoundVars, bVars, true);

+        locals.AddRange(bVars);

+        var havocIds = new Bpl.IdentifierExprSeq();

+        foreach (Bpl.Variable bv in bVars) {

+          havocIds.Add(new Bpl.IdentifierExpr(s.Tok, bv));

+        }

+        definedness.Add(new Bpl.HavocCmd(s.Tok, havocIds));

+        definedness.Add(new Bpl.AssumeCmd(s.Tok, typeAntecedent));

+      }

       TrStmt_CheckWellformed(s.Range, definedness, locals, etran, false);

       definedness.Add(new Bpl.AssumeCmd(s.Range.tok, etran.TrExpr(s.Range)));

 

@@ -5474,22 +5490,17 @@ namespace Microsoft.Dafny {
       var initEtran = new ExpressionTranslator(this, predef, initHeap, etran.Old.HeapExpr);

       // initHeap := $Heap;

       exporter.Add(Bpl.Cmd.SimpleAssign(s.Tok, initHeap, etran.HeapExpr));

-      if (s.Ens.Exists(ens => MentionsOldState(ens.E))) {

-        // advance $Heap;

-        exporter.Add(new Bpl.HavocCmd(s.Tok, new Bpl.IdentifierExprSeq((Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)etran.HeapExpr, etran.Tick())));

-        foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(s.Tok, new List<FrameExpression>(), initEtran, etran, initEtran)) {

-          if (tri.IsFree) {

-            exporter.Add(new Bpl.AssumeCmd(s.Tok, tri.Expr));

-          }

+      // advance $Heap;

+      exporter.Add(new Bpl.HavocCmd(s.Tok, new Bpl.IdentifierExprSeq((Bpl.IdentifierExpr/*TODO: this cast is rather dubious*/)etran.HeapExpr, etran.Tick())));

+      foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(s.Tok, new List<FrameExpression>(), s.IsGhost, initEtran, etran, initEtran)) {

+        if (tri.IsFree) {

+          exporter.Add(new Bpl.AssumeCmd(s.Tok, tri.Expr));

         }

-      } else {

-        // As an optimization, create the illusion that the $Heap is unchanged by the forall-statement body.

-        exporter.Add(new Bpl.HavocCmd(s.Tok, new Bpl.IdentifierExprSeq(etran.Tick())));

       }

 

-      bvars = new Bpl.VariableSeq();

+      var bvars = new Bpl.VariableSeq();

       Dictionary<IVariable, Expression> substMap;

-      ante = initEtran.TrBoundVariablesRename(s.BoundVars, bvars, out substMap);

+      var ante = initEtran.TrBoundVariablesRename(s.BoundVars, bvars, out substMap);

       var range = Substitute(s.Range, null, substMap);

       ante = BplAnd(ante, initEtran.TrExpr(range));

 

@@ -5608,7 +5619,7 @@ namespace Microsoft.Dafny {
         TrStmt_CheckWellformed(e, invDefinednessBuilder, locals, etran, true);

       }

       // include boilerplate invariants

-      foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(s.Tok, codeContext.Modifies.Expressions, etranPreLoop, etran, etran.Old))

+      foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(s.Tok, codeContext.Modifies.Expressions, s.IsGhost, etranPreLoop, etran, etran.Old))

       {

           if (tri.IsFree) {

               invariants.Add(new Bpl.AssumeCmd(s.Tok, tri.Expr));

@@ -8406,6 +8417,7 @@ namespace Microsoft.Dafny {
 

       IsGoodHeap,

       HeapSucc,

+      HeapSuccGhost,

 

       DynamicType,  // allocated type (of object reference)

       DtType,       // type of datatype value

@@ -8415,6 +8427,7 @@ namespace Microsoft.Dafny {
       DeclType,

       FieldOfDecl,

       FDim,  // field dimension (0 - named, 1 or more - indexed)

+      IsGhostField,

 

       DatatypeCtorId,

       DtRank,

@@ -8627,6 +8640,10 @@ namespace Microsoft.Dafny {
           Contract.Assert(args.Length == 2);

           Contract.Assert(typeInstantiation == null);

           return FunctionCall(tok, "$HeapSucc", Bpl.Type.Bool, args);

+        case BuiltinFunction.HeapSuccGhost:

+          Contract.Assert(args.Length == 2);

+          Contract.Assert(typeInstantiation == null);

+          return FunctionCall(tok, "$HeapSuccGhost", Bpl.Type.Bool, args);

 

         case BuiltinFunction.DynamicType:

           Contract.Assert(args.Length == 1);

@@ -8660,6 +8677,10 @@ namespace Microsoft.Dafny {
           Contract.Assert(args.Length == 1);

           Contract.Assert(typeInstantiation != null);

           return FunctionCall(tok, "FDim", Bpl.Type.Int, args);

+        case BuiltinFunction.IsGhostField:

+          Contract.Assert(args.Length == 1);

+          Contract.Assert(typeInstantiation != null);

+          return FunctionCall(tok, "$IsGhostField", Bpl.Type.Bool, args);

 

         case BuiltinFunction.DatatypeCtorId:

           Contract.Assert(args.Length == 1);

@@ -9556,22 +9577,6 @@ namespace Microsoft.Dafny {
       }

     }

 

-    /// <summary>

-    /// Returns true iff 'expr' is a two-state expression, that is, if it mentions "old(...)" or "fresh(...)".

-    /// </summary>

-    public static bool MentionsOldState(Expression expr) {

-      Contract.Requires(expr != null);

-      if (expr is OldExpr || expr is FreshExpr) {

-        return true;

-      }

-      foreach (var ee in expr.SubExpressions) {

-        if (MentionsOldState(ee)) {

-          return true;

-        }

-      }

-      return false;

-    }

-

     public static Expression Substitute(Expression expr, Expression receiverReplacement, Dictionary<IVariable, Expression/*!*/>/*!*/ substMap) {

       Contract.Requires(expr != null);

       Contract.Requires(cce.NonNullDictionaryAndValues(substMap));

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 92b575aa..42989a5a 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -213,6 +213,21 @@ Execution trace:
 SmallTests.dfy(375,6): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

     (0,0): anon3_Else

+SmallTests.dfy(638,14): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    SmallTests.dfy(635,5): anon7_LoopHead

+    (0,0): anon7_LoopBody

+    SmallTests.dfy(635,5): anon8_Else

+    (0,0): anon3

+    (0,0): anon9_Then

+    (0,0): anon6

+SmallTests.dfy(659,14): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon7_Then

+    (0,0): anon8_Then

+    (0,0): anon3

 SmallTests.dfy(285,3): Error BP5003: A postcondition might not hold on this return path.

 SmallTests.dfy(279,11): Related location: This is the postcondition that might not hold.

 Execution trace:

@@ -296,7 +311,7 @@ Execution trace:
     (0,0): anon0

     (0,0): anon5_Else

 

-Dafny program verifier finished with 75 verified, 29 errors

+Dafny program verifier finished with 81 verified, 31 errors

 

 -------------------- Definedness.dfy --------------------

 Definedness.dfy(8,7): Error: possible division by zero

@@ -510,6 +525,18 @@ ResolutionErrors.dfy(502,7): Error: RHS (of type List<A>) not assignable to LHS
 ResolutionErrors.dfy(516,23): Error: type of case bodies do not agree (found Tree<_T1,_T0>, previous types Tree<_T0,_T1>)

 ResolutionErrors.dfy(528,24): Error: Wrong number of type arguments (0 instead of 2) passed to class/datatype: Tree

 ResolutionErrors.dfy(563,18): Error: type of bound variable 'z' could not determined; please specify the type explicitly

+ResolutionErrors.dfy(576,13): Error: 'new' is not allowed in ghost contexts

+ResolutionErrors.dfy(577,9): Error: 'new' is not allowed in ghost contexts

+ResolutionErrors.dfy(584,14): Error: new allocation not supported in forall statements

+ResolutionErrors.dfy(589,11): Error: the body of the enclosing forall statement is not allowed to update heap locations

+ResolutionErrors.dfy(589,14): Error: new allocation not allowed in ghost context

+ResolutionErrors.dfy(599,23): Error: 'new' is not allowed in ghost contexts

+ResolutionErrors.dfy(606,15): Error: 'new' is not allowed in ghost contexts

+ResolutionErrors.dfy(606,15): Error: only ghost methods can be called from this context

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

+ResolutionErrors.dfy(615,17): Error: 'new' is not allowed in ghost contexts

+ResolutionErrors.dfy(617,20): Error: only ghost methods can be called from this context

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

 ResolutionErrors.dfy(427,2): Error: More than one default constructor

 ResolutionErrors.dfy(48,13): Error: 'this' is not allowed in a 'static' context

 ResolutionErrors.dfy(109,9): Error: ghost variables are allowed only in specification contexts

@@ -582,7 +609,7 @@ ResolutionErrors.dfy(541,7): Error: let-such-that expressions are allowed only i
 ResolutionErrors.dfy(541,20): Error: ghost variables are allowed only in specification contexts

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

 ResolutionErrors.dfy(544,18): Error: unresolved identifier: w

-77 resolution/type errors detected in ResolutionErrors.dfy

+89 resolution/type errors detected in ResolutionErrors.dfy

 

 -------------------- ParseErrors.dfy --------------------

 ParseErrors.dfy(4,19): error: a chain cannot have more than one != operator

@@ -1131,22 +1158,28 @@ Dafny program verifier finished with 27 verified, 6 errors
 

 -------------------- ParallelResolveErrors.dfy --------------------

 ParallelResolveErrors.dfy(7,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(17,6): Error: LHS of assignment must denote a mutable variable or field

-ParallelResolveErrors.dfy(22,6): Error: body of forall statement is attempting to update a variable declared outside the forall statement

-ParallelResolveErrors.dfy(40,6): 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)

-ParallelResolveErrors.dfy(52,13): Error: set choose operator not supported inside the enclosing forall statement

-ParallelResolveErrors.dfy(57,13): Error: new allocation not supported in forall statements

-ParallelResolveErrors.dfy(67,6): Error: the body of the enclosing forall statement is not allowed to call non-ghost methods

-ParallelResolveErrors.dfy(74,19): Error: trying to break out of more loop levels than there are enclosing loops

-ParallelResolveErrors.dfy(78,18): Error: return statement is not allowed inside a forall statement

-ParallelResolveErrors.dfy(85,21): Error: trying to break out of more loop levels than there are enclosing loops

-ParallelResolveErrors.dfy(86,20): Error: trying to break out of more loop levels than there are enclosing loops

-ParallelResolveErrors.dfy(87,20): Error: break label is undefined or not in scope: OutsideLoop

-ParallelResolveErrors.dfy(96,24): Error: trying to break out of more loop levels than there are enclosing loops

-ParallelResolveErrors.dfy(97,24): Error: break label is undefined or not in scope: OutsideLoop

-ParallelResolveErrors.dfy(105,2): Warning: the conclusion of the body of this forall statement will not be known outside the forall statement; consider using an 'ensures' clause

-ParallelResolveErrors.dfy(106,9): Error: the body of the enclosing forall statement is not allowed to update heap locations

-15 resolution/type errors detected in ParallelResolveErrors.dfy

+ParallelResolveErrors.dfy(18,6): Error: LHS of assignment must denote a mutable variable or field

+ParallelResolveErrors.dfy(23,6): Error: body of forall statement is attempting to update a variable declared outside the forall statement

+ParallelResolveErrors.dfy(41,6): 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)

+ParallelResolveErrors.dfy(53,13): Error: set choose operator not supported inside the enclosing forall statement

+ParallelResolveErrors.dfy(58,13): Error: new allocation not supported in forall statements

+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,13): Error: new allocation not allowed in ghost context

+ParallelResolveErrors.dfy(66,13): Error: new allocation not allowed in ghost context

+ParallelResolveErrors.dfy(67,6): 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(68,6): Error: the body of the enclosing forall statement is not allowed to call non-ghost methods

+ParallelResolveErrors.dfy(75,19): Error: trying to break out of more loop levels than there are enclosing loops

+ParallelResolveErrors.dfy(79,18): Error: return statement is not allowed inside a forall statement

+ParallelResolveErrors.dfy(86,21): Error: trying to break out of more loop levels than there are enclosing loops

+ParallelResolveErrors.dfy(87,20): Error: trying to break out of more loop levels than there are enclosing loops

+ParallelResolveErrors.dfy(88,20): Error: break label is undefined or not in scope: OutsideLoop

+ParallelResolveErrors.dfy(97,24): Error: trying to break out of more loop levels than there are enclosing loops

+ParallelResolveErrors.dfy(98,24): Error: break label is undefined or not in scope: OutsideLoop

+ParallelResolveErrors.dfy(109,9): Error: the body of the enclosing forall statement is not allowed to update heap locations

+ParallelResolveErrors.dfy(117,6): 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(122,6): 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

 

 -------------------- Parallel.dfy --------------------

 Parallel.dfy(31,5): Error BP5002: A precondition for this call might not hold.

@@ -1226,33 +1259,13 @@ Execution trace:
     (0,0): anon19_Then

     (0,0): anon20_Then

     (0,0): anon5

-Parallel.dfy(214,10): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon4_Else

-    (0,0): anon3

-Parallel.dfy(226,10): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon4_Else

-    (0,0): anon3

-Parallel.dfy(254,10): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon6_Else

-    (0,0): anon5

-Parallel.dfy(270,10): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-    (0,0): anon6_Else

-    (0,0): anon5

-Parallel.dfy(307,10): Error: assertion violation

+Parallel.dfy(293,10): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon4_Else

     (0,0): anon3

 

-Dafny program verifier finished with 41 verified, 13 errors

+Dafny program verifier finished with 40 verified, 9 errors

 

 -------------------- TypeParameters.dfy --------------------

 TypeParameters.dfy(44,22): Error: assertion violation

@@ -2015,6 +2028,21 @@ Execution trace:
 SmallTests.dfy(375,6): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

     (0,0): anon3_Else

+SmallTests.dfy(638,14): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    SmallTests.dfy(635,5): anon7_LoopHead

+    (0,0): anon7_LoopBody

+    SmallTests.dfy(635,5): anon8_Else

+    (0,0): anon3

+    (0,0): anon9_Then

+    (0,0): anon6

+SmallTests.dfy(659,14): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon7_Then

+    (0,0): anon8_Then

+    (0,0): anon3

 SmallTests.dfy(285,3): Error BP5003: A postcondition might not hold on this return path.

 SmallTests.dfy(279,11): Related location: This is the postcondition that might not hold.

 Execution trace:

@@ -2098,7 +2126,7 @@ Execution trace:
     (0,0): anon0

     (0,0): anon5_Else

 

-Dafny program verifier finished with 75 verified, 29 errors

+Dafny program verifier finished with 81 verified, 31 errors

 out.tmp.dfy(33,11): Error: index out of range

 Execution trace:

     (0,0): anon0

@@ -2178,8 +2206,23 @@ Execution trace:
 out.tmp.dfy(285,6): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

     (0,0): anon3_Else

-out.tmp.dfy(401,3): Error BP5003: A postcondition might not hold on this return path.

-out.tmp.dfy(395,11): Related location: This is the postcondition that might not hold.

+out.tmp.dfy(386,14): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    out.tmp.dfy(382,5): anon7_LoopHead

+    (0,0): anon7_LoopBody

+    out.tmp.dfy(382,5): anon8_Else

+    (0,0): anon3

+    (0,0): anon9_Then

+    (0,0): anon6

+out.tmp.dfy(412,14): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon7_Then

+    (0,0): anon8_Then

+    (0,0): anon3

+out.tmp.dfy(449,3): Error BP5003: A postcondition might not hold on this return path.

+out.tmp.dfy(443,11): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

     (0,0): anon18_Else

@@ -2188,27 +2231,27 @@ Execution trace:
     (0,0): anon24_Then

     (0,0): anon15

     (0,0): anon25_Else

-out.tmp.dfy(425,12): Error: assertion violation

+out.tmp.dfy(473,12): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon8_Then

     (0,0): anon7

-out.tmp.dfy(430,10): Error: assertion violation

+out.tmp.dfy(478,10): Error: assertion violation

 Execution trace:

     (0,0): anon0

-out.tmp.dfy(440,4): Error: cannot prove termination; try supplying a decreases clause

+out.tmp.dfy(488,4): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

     (0,0): anon3_Else

-out.tmp.dfy(448,10): Error BP5003: A postcondition might not hold on this return path.

-out.tmp.dfy(449,41): Related location: This is the postcondition that might not hold.

+out.tmp.dfy(496,10): Error BP5003: A postcondition might not hold on this return path.

+out.tmp.dfy(497,41): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon6_Else

-out.tmp.dfy(486,12): Error: assertion violation

+out.tmp.dfy(534,12): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon3_Then

     (0,0): anon2

-out.tmp.dfy(500,20): Error: left-hand sides 0 and 1 may refer to the same location

+out.tmp.dfy(548,20): Error: left-hand sides 0 and 1 may refer to the same location

 Execution trace:

     (0,0): anon0

     (0,0): anon27_Then

@@ -2220,11 +2263,11 @@ Execution trace:
     (0,0): anon31_Then

     (0,0): anon32_Then

     (0,0): anon12

-out.tmp.dfy(502,15): Error: left-hand sides 1 and 2 may refer to the same location

+out.tmp.dfy(550,15): Error: left-hand sides 1 and 2 may refer to the same location

 Execution trace:

     (0,0): anon0

     (0,0): anon27_Then

-    out.tmp.dfy(495,17): anon28_Else

+    out.tmp.dfy(543,17): anon28_Else

     (0,0): anon4

     (0,0): anon29_Else

     (0,0): anon7

@@ -2236,13 +2279,13 @@ Execution trace:
     (0,0): anon37_Then

     (0,0): anon22

     (0,0): anon38_Then

-out.tmp.dfy(509,25): Error: target object may be null

+out.tmp.dfy(557,25): Error: target object may be null

 Execution trace:

     (0,0): anon0

-out.tmp.dfy(523,10): Error: assertion violation

+out.tmp.dfy(570,10): Error: assertion violation

 Execution trace:

     (0,0): anon0

-out.tmp.dfy(550,10): Error: assertion violation

+out.tmp.dfy(597,10): Error: assertion violation

 Execution trace:

     (0,0): anon0

     (0,0): anon8_Then

@@ -2250,18 +2293,18 @@ Execution trace:
     (0,0): anon4

     (0,0): anon10_Then

     (0,0): anon7

-out.tmp.dfy(564,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

+out.tmp.dfy(611,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

 Execution trace:

     (0,0): anon0

     (0,0): anon5_Then

     (0,0): anon6_Then

     (0,0): anon3

-out.tmp.dfy(566,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

+out.tmp.dfy(613,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate

 Execution trace:

     (0,0): anon0

     (0,0): anon5_Else

 

-Dafny program verifier finished with 75 verified, 29 errors

+Dafny program verifier finished with 81 verified, 31 errors

 

 -------------------- LetExpr.dfy --------------------

 LetExpr.dfy(5,12): Error: assertion violation

diff --git a/Test/dafny0/Parallel.dfy b/Test/dafny0/Parallel.dfy
index 37004441..4a9c0a31 100644
--- a/Test/dafny0/Parallel.dfy
+++ b/Test/dafny0/Parallel.dfy
@@ -203,27 +203,15 @@ method OmittedRange() {
 

 class TwoState_C { ghost var data: int; }

 

+// It is not possible to achieve this postcondition in a ghost method, because ghost

+// contexts are not allowed to allocate state.  Callers of this ghost method will know

+// that the postcondition is tantamount to 'false'.

 ghost static method TwoState0(y: int)

   ensures exists o: TwoState_C :: o != null && fresh(o);

-{

-  var p := new TwoState_C;

-}

 

 method TwoState_Main0() {

   forall (x) { TwoState0(x); }

-  assert false;  // error: this location is indeed reachable (if the translation before it is sound)

-}

-

-ghost static method TwoState1(y: int)

-  ensures exists c: TwoState_C :: c != null && c.data != old(c.data);

-{

-  var c := new TwoState_C;

-  c.data := c.data + 1;

-}

-

-method TwoState_Main1() {

-  forall (x) { TwoState1(x); }

-  assert false;  // error: this location is indeed reachable (if the translation before it is sound)

+  assert false;  // no prob, because the postcondition of TwoState0 implies false

 }

 

 method X_Legit(c: TwoState_C)

@@ -242,8 +230,6 @@ method X_Legit(c: TwoState_C)
 // However, there's an important difference in the translation, which is that the

 // occurrence of 'fresh' here refers to the initial state of the TwoStateMain2

 // method, not the beginning of the 'forall' statement.

-// Still, care needs to be taken in the translation to make sure that the forall

-// statement's effect on the heap is not optimized away.

 method TwoState_Main2()

 {

   forall (x: int)

@@ -251,12 +237,12 @@ method TwoState_Main2()
   {

     TwoState0(x);

   }

-  assert false;  // error: this location is indeed reachable (if the translation before it is sound)

+  assert false;  // fine, for the postcondition of the forall statement implies false

 }

 

 // At first glance, this looks like an inlined version of TwoState_Main0 above.

 // However, there's an important difference in the translation, which is that the

-// occurrence of 'fresh' here refers to the initial state of the TwoStateMain3

+// occurrence of 'fresh' here refers to the initial state of the TwoState_Main3

 // method, not the beginning of the 'forall' statement.

 // Still, care needs to be taken in the translation to make sure that the forall

 // statement's effect on the heap is not optimized away.

@@ -265,9 +251,9 @@ method TwoState_Main3()
   forall (x: int)

     ensures exists o: TwoState_C :: o != null && fresh(o);

   {

-    var p := new TwoState_C;

+    assume false;  // (there's no other way to achieve this forall-statement postcondition)

   }

-  assert false;  // error: this location is indeed reachable (if the translation before it is sound)

+  assert false;  // it is known that the forall's postcondition is contradictory, so this assert is fine

 }

 

 // ------- empty forall statement -----------------------------------------

diff --git a/Test/dafny0/ParallelResolveErrors.dfy b/Test/dafny0/ParallelResolveErrors.dfy
index c740f88c..d3bfe97b 100644
--- a/Test/dafny0/ParallelResolveErrors.dfy
+++ b/Test/dafny0/ParallelResolveErrors.dfy
@@ -9,6 +9,7 @@ class C {
   }

   ghost method Init_ModifyStuff(c: C) modifies this, c; { }

   method NonGhostMethod() { print "hello\n"; }

+  ghost method GhostMethodWithModifies(x: int) modifies this; { gdata := gdata + x; }

 }

 

 method M0(IS: set<int>)

@@ -59,11 +60,11 @@ method M0(IS: set<int>)
   forall (i | 0 <= i < 20)

     ensures true;

   {

-    var c := new C;  // allowed

-    var d := new C.Init_ModifyNothing();

-    var e := new C.Init_ModifyThis();

-    var f := new C.Init_ModifyStuff(e);

-    c.Init_ModifyStuff(d);

+    var c := new C;  // error: 'new' not allowed in ghost context

+    var d := new C.Init_ModifyNothing();  // error: 'new' not allowed in ghost context

+    var e := new C.Init_ModifyThis();  // error: 'new' not allowed in ghost context

+    var f := new C.Init_ModifyStuff(e);  // error: 'new' not allowed in ghost context

+    c.Init_ModifyStuff(d);  // error: not allowed to call method with modifies clause in ghost context

     c.NonGhostMethod();  // error: only allowed to call ghost methods (because of possible 'print' statements, sigh)

   }

 }

@@ -102,7 +103,22 @@ method M1() {
 

 method M2() {

   var a := new int[100];

-  forall (x | 0 <= x < 100) {

-    a[x] :| assume a[x] > 0;  // error: not allowed to update heap location in a forall statement with an assume

+  forall (x | 0 <= x < 100)

+    ensures true;

+  {

+    a[x] :| assume a[x] > 0;  // error: not allowed to update heap location in a proof-forall statement

+  }

+}

+

+method M3(c: C)

+  requires c != null;

+{

+  forall x {

+    c.GhostMethodWithModifies(x);  // error: not allowed to call method with nonempty modifies clause

+  }

+  forall x

+    ensures true;

+  {

+    c.GhostMethodWithModifies(x);  // error: not allowed to call method with nonempty modifies clause

   }

 }

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 5ad6d1fe..696a583f 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -563,3 +563,66 @@ module NonInferredType {
     assume forall z :: P(z) && z == t;  // error: the type of z is not determined

   }

 }

+

+// ------------ Here are some tests that ghost contexts don't allocate objects -------------

+

+module GhostAllocationTests {

+  class G { }

+  iterator GIter() { }

+

+  ghost method GhostNew0()

+    ensures exists o: G :: o != null && fresh(o);

+  {

+    var p := new G;  // error: ghost context is not allowed to allocate state

+    p := new G;  // error: ditto

+  }

+

+  method GhostNew1(n: nat)

+  {

+    var a := new G[n];

+    forall i | 0 <= i < n {

+      a[i] := new G;  // error: 'new' is currently not supported in forall statements

+    }

+    forall i | 0 <= i < n

+      ensures true;  // this makes the whole 'forall' statement into a ghost statement

+    {

+      a[i] := new G;  // error: 'new' not allowed in ghost contexts, and proof-forall cannot update state

+    }

+  }

+

+  method GhostNew2(n: nat, ghost g: int) returns (t: G, z: int)

+  {

+    if n < 0 {

+      z, t := 5, new G;  // fine

+    }

+    if n < g {

+      var zz, tt := 5, new G;  // error: 'new' not allowed in ghost contexts

+    }

+  }

+

+  method GhostNew3(ghost b: bool)

+  {

+    if (b) {

+      var y := new GIter();  // error: 'new' not allowed in ghost contexts (and a non-ghost method is not allowed to be called here either)

+    }

+  }

+

+  method GhostNew4(n: nat)

+  {

+    var g := new G;

+    calc {

+      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

+      1 + 4;

+      { GhostNew5(g); }  // error: cannot call method with nonempty modifies

+      -5 + 10;

+    }

+  }

+

+  ghost method GhostNew5(g: G)

+    modifies g;

+  {

+  }

+}

diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index 2f12fdd2..d9b91763 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -571,8 +571,8 @@ method AssignSuchThat4()
 

 method AssignSuchThat5()

 {

-  ghost var n := new Node;

-  n :| fresh(n);  // fine

+  var k := new Node;

+  ghost var n: Node :| fresh(n);  // fine

   assert false;  // error

 }

 

@@ -621,3 +621,45 @@ method LetSuchThat2(n: nat)
   }

 }

 

+// ------------- ghost loops only modify ghost fields

+

+class GT {

+  var x: int;

+  var y: int;

+  ghost var z: int;

+  method M0(N: int)

+    modifies this;

+  {

+    x := 18;

+    var n := 0;

+    while n < 100 {  // not a ghost loop

+      n, y := n + 1, y + 1;

+    }

+    assert x == 18;  // error: the verifier loses this information for the loop

+  }

+  method M1(ghost N: int)

+    modifies this;

+  {

+    x := 18;

+    ghost var n := N;

+    while n < 100 {  // a ghost loop

+      n, z := n + 1, z + 1;

+    }

+    assert x == 18;  // fine, the verifier knows that the loop modifies only ghost state

+  }

+  method P0()

+    modifies this;

+  ghost method P1()

+    modifies this;

+  method Q()

+    modifies this;

+  {

+    if (*) {

+      P0();

+      assert forall x: GT :: x != null ==> !fresh(x);  // error: method P2 may have allocated stuff

+    } else {

+      P1();

+      assert forall x: GT :: x != null ==> !fresh(x);  // fine, because the ghost method does not allocate anything

+    }

+  }

+}