Dafny: removed allocated, changed semantics of fresh

-allocated(x) removed, as really only useful in old(...)
-old(allocated(x)) and !fresh(x) are equivalent (for x with type ref, set, sequence, and datatype).

1 files changed, 0 insertions, 20 deletions

diff --git a/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index bf2c7492..a019f068 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/Dafny/DafnyAst.cs
@@ -3125,26 +3125,6 @@ namespace Microsoft.Dafny {
     }

   }

 

-  public class AllocatedExpr : Expression

-  {

-    public readonly Expression E;

-    [ContractInvariantMethod]

-    void ObjectInvariant() {

-      Contract.Invariant(E != null);

-    }

-

-    public AllocatedExpr(IToken tok, Expression expr)

-      : base(tok) {

-      Contract.Requires(tok != null);

-      Contract.Requires(expr != null);

-      E = expr;

-    }

-

-    public override IEnumerable<Expression> SubExpressions {

-      get { yield return E; }

-    }

-  }

-

   public class UnaryExpr : Expression

   {

     public enum Opcode {