Dafny:

* Big change:  Add type and allocatedness information everywhere in the Boogie translation.  This not only fixes some potential soundness problems (see Test/dafny1/TypeAntecedents.dfy), but it also gives more information about the program.  On the downside, it also requires discharging more antecedents in order to use some axioms.  Another downside is that overall performance has gone down (however, this may be just an indirect consequence of the change, as it was in one investigated case).

* Increase the applicability of function axioms (extending the coarse-grain function/module height mechanism used as an antecedent of function axioms).  (Internally, this uses the new canCall mechanism.)

* Extend language with "allocated( Expr )" expressions, which for any type of expression "Expr" says that "Expr" is allocated and has the expected type.

* More details error messages about ill-defined expressions (internally, by using CheckWellformedness instead of "assert IsTotal")

* Add axioms about idempotence of set union and intersection

* The compiler does not support (the experimental feature) coupling invariants, so generate error if the compiler ever gets one

* In the implementation, combine common behavior of MatchCaseStmt and MatchCaseExpr into a superclass MatchCase

* Fixed error in translation of while(*)

24 files changed, 1349 insertions, 633 deletions

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 6c9faa29..1ef8aea7 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -51,6 +51,15 @@ function Set#Intersection<T>(Set T, Set T) returns (Set T);
 axiom (forall<T> a: Set T, b: Set T, o: T :: { Set#Intersection(a,b)[o] }

   Set#Intersection(a,b)[o] <==> a[o] && b[o]);

 

+axiom (forall<T> a, b: Set T :: { Set#Union(Set#Union(a, b), b) }

+  Set#Union(Set#Union(a, b), b) == Set#Union(a, b));

+axiom (forall<T> a, b: Set T :: { Set#Union(a, Set#Union(a, b)) }

+  Set#Union(a, Set#Union(a, b)) == Set#Union(a, b));

+axiom (forall<T> a, b: Set T :: { Set#Intersection(Set#Intersection(a, b), b) }

+  Set#Intersection(Set#Intersection(a, b), b) == Set#Intersection(a, b));

+axiom (forall<T> a, b: Set T :: { Set#Intersection(a, Set#Intersection(a, b)) }

+  Set#Intersection(a, Set#Intersection(a, b)) == Set#Intersection(a, b));

+

 function Set#Difference<T>(Set T, Set T) returns (Set T);

 axiom (forall<T> a: Set T, b: Set T, o: T :: { Set#Difference(a,b)[o] }

   Set#Difference(a,b)[o] <==> a[o] && !b[o]);

@@ -205,8 +214,8 @@ const unique class.bool: ClassName;
 const unique class.set: ClassName;

 const unique class.seq: ClassName;

 

-function dtype(ref) returns (ClassName);

-function TypeParams(ref, int) returns (ClassName);

+function /*{:never_pattern true}*/ dtype(ref) returns (ClassName);

+function /*{:never_pattern true}*/ TypeParams(ref, int) returns (ClassName);

 

 function TypeTuple(a: ClassName, b: ClassName) returns (ClassName);

 function TypeTupleCar(ClassName) returns (ClassName);

@@ -222,6 +231,9 @@ axiom (forall a: ClassName, b: ClassName :: { TypeTuple(a,b) }
 

 type DatatypeType;

 

+function /*{:never_pattern true}*/ DtType(DatatypeType) returns (ClassName);  // the analog of dtype for datatype values

+function /*{:never_pattern true}*/ DtTypeParams(DatatypeType, int) returns (ClassName);  // the analog of TypeParams

+

 type DtCtorId;

 function DatatypeCtorId(DatatypeType) returns (DtCtorId);

 

@@ -244,9 +256,6 @@ type Field alpha;
 

 function FDim<T>(Field T): int;

 

-const unique alloc: Field bool;

-axiom FDim(alloc) == 0;

-

 function IndexField(int): Field BoxType;

 axiom (forall i: int :: { IndexField(i) } FDim(IndexField(i)) == 1);

 function IndexField_Inverse<T>(Field T): int;

@@ -264,6 +273,50 @@ axiom (forall f: Field BoxType, i: int :: { MultiIndexField(f,i) }
 function DeclType<T>(Field T) returns (ClassName);

 

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

+// -- Allocatedness ----------------------------------------------

+// ---------------------------------------------------------------

+

+const unique alloc: Field bool;

+axiom FDim(alloc) == 0;

+

+function DtAlloc(DatatypeType, HeapType): bool;

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

+  { $HeapSucc(h, k), DtAlloc(d, h) }

+  { $HeapSucc(h, k), DtAlloc(d, k) }

+  $HeapSucc(h, k) ==> DtAlloc(d, h) ==> DtAlloc(d, k));

+

+function GenericAlloc(BoxType, HeapType): bool;

+axiom (forall h: HeapType, k: HeapType, d: BoxType ::

+  { $HeapSucc(h, k), GenericAlloc(d, h) }

+  { $HeapSucc(h, k), GenericAlloc(d, k) }

+  $HeapSucc(h, k) ==> GenericAlloc(d, h) ==> GenericAlloc(d, k));

+// GenericAlloc ==>

+axiom (forall b: BoxType, h: HeapType ::

+  { GenericAlloc(b, h), h[$Unbox(b): ref, alloc] }

+  GenericAlloc(b, h) ==>

+  $Unbox(b): ref == null || h[$Unbox(b): ref, alloc]);

+axiom (forall b: BoxType, h: HeapType, i: int ::

+  { GenericAlloc(b, h), Seq#Index($Unbox(b): Seq BoxType, i) }

+  GenericAlloc(b, h) &&

+  0 <= i && i < Seq#Length($Unbox(b): Seq BoxType) ==>

+  GenericAlloc( Seq#Index($Unbox(b): Seq BoxType, i), h ) );

+axiom (forall b: BoxType, h: HeapType, t: BoxType ::

+  { GenericAlloc(b, h), ($Unbox(b): Set BoxType)[t] }

+  GenericAlloc(b, h) && ($Unbox(b): Set BoxType)[t] ==>

+  GenericAlloc(t, h));

+axiom (forall b: BoxType, h: HeapType ::

+  { GenericAlloc(b, h), DtType($Unbox(b): DatatypeType) }

+  GenericAlloc(b, h) ==> DtAlloc($Unbox(b): DatatypeType, h));

+// ==> GenericAlloc

+axiom (forall b: bool, h: HeapType ::

+  $IsGoodHeap(h) ==> GenericAlloc($Box(b), h));

+axiom (forall x: int, h: HeapType ::

+  $IsGoodHeap(h) ==> GenericAlloc($Box(x), h));

+axiom (forall r: ref, h: HeapType ::

+  { GenericAlloc($Box(r), h) }

+  $IsGoodHeap(h) && (r == null || h[r,alloc]) ==> GenericAlloc($Box(r), h));

+

+// ---------------------------------------------------------------

 // -- Arrays -----------------------------------------------------

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

 

diff --git a/Dafny/Compiler.cs b/Dafny/Compiler.cs
index a00ca0b0..dc7caac7 100644
--- a/Dafny/Compiler.cs
+++ b/Dafny/Compiler.cs
@@ -445,6 +445,9 @@ namespace Microsoft.Dafny {
             }

           }

 

+        } else if (member is CouplingInvariant) {

+          Error("coupling invariants are not supported in compilation");

+

         } else {

           Contract.Assert(false); throw new cce.UnreachableException();  // unexpected member

         }

diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg
index ef7164bc..c4955a6a 100644
--- a/Dafny/Dafny.atg
+++ b/Dafny/Dafny.atg
@@ -1188,6 +1188,8 @@ ConstAtomExpression<out Expression/*!*/ e>
     ")" ]                                      (. e = new DatatypeValue(t, dtName.val, id.val, elements); .)

   | "fresh"                                    (. x = t; .)

     "(" Expression<out e> ")"                  (. e = new FreshExpr(x, e); .)

+  | "allocated"                                (. x = t; .)

+    "(" Expression<out e> ")"                  (. e = new AllocatedExpr(x, e); .)

   | "|"                                        (. x = t; .)

       Expression<out e>                        (. e = new UnaryExpr(x, UnaryExpr.Opcode.SeqLength, e); .)

     "|"

diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs
index 9eec1e39..1ae19313 100644
--- a/Dafny/DafnyAst.cs
+++ b/Dafny/DafnyAst.cs
@@ -1622,30 +1622,22 @@ namespace Microsoft.Dafny {
     }

   }

 

-  public class MatchCaseStmt {

-    public readonly IToken tok;

-    public readonly string Id;

-    public DatatypeCtor Ctor;  // filled in by resolution

-    public readonly List<BoundVar/*!*/>/*!*/ Arguments;

+  public class MatchCaseStmt : MatchCase

+  {

     public readonly List<Statement/*!*/>/*!*/ Body;

 

     [ContractInvariantMethod]

     void ObjectInvariant() {

-      Contract.Invariant(tok != null);

-      Contract.Invariant(Id != null);

-      Contract.Invariant(cce.NonNullElements(Arguments));

       Contract.Invariant(cce.NonNullElements(Body));

     }

 

-

-    public MatchCaseStmt(IToken tok, string id, [Captured] List<BoundVar/*!*/>/*!*/ arguments, [Captured] List<Statement/*!*/>/*!*/ body) {

+    public MatchCaseStmt(IToken tok, string id, [Captured] List<BoundVar/*!*/>/*!*/ arguments, [Captured] List<Statement/*!*/>/*!*/ body)

+      : base(tok, id, arguments)

+    {

       Contract.Requires(tok != null);

       Contract.Requires(id != null);

       Contract.Requires(cce.NonNullElements(arguments));

       Contract.Requires(cce.NonNullElements(body));

-      this.tok = tok;

-      this.Id = id;

-      this.Arguments = arguments;

       this.Body = body;

     }

   }

@@ -1989,11 +1981,27 @@ namespace Microsoft.Dafny {
       Contract.Requires(tok != null);

       Contract.Requires(expr != null);

       E = expr;

+    }

+  }

 

+  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 class UnaryExpr : Expression {

+  public class UnaryExpr : Expression

+  {

     public enum Opcode {

       Not,

       SeqLength

@@ -2266,29 +2274,44 @@ namespace Microsoft.Dafny {
     }

   }

 

-  public class MatchCaseExpr {

+  public abstract class MatchCase

+  {

     public readonly IToken tok;

     public readonly string Id;

     public DatatypeCtor Ctor;  // filled in by resolution

     public readonly List<BoundVar/*!*/>/*!*/ Arguments;

-    public readonly Expression/*!*/ Body;

     [ContractInvariantMethod]

     void ObjectInvariant() {

       Contract.Invariant(tok != null);

       Contract.Invariant(Id != null);

-      Contract.Invariant(Body != null);

       Contract.Invariant(cce.NonNullElements(Arguments));

     }

 

-

-    public MatchCaseExpr(IToken tok, string id, [Captured] List<BoundVar/*!*/>/*!*/ arguments, Expression body) {

+    public MatchCase(IToken tok, string id, [Captured] List<BoundVar/*!*/>/*!*/ arguments) {

       Contract.Requires(tok != null);

       Contract.Requires(id != null);

       Contract.Requires(cce.NonNullElements(arguments));

-      Contract.Requires(body != null);

       this.tok = tok;

       this.Id = id;

       this.Arguments = arguments;

+    }

+  }

+

+  public class MatchCaseExpr : MatchCase

+  {

+    public readonly Expression/*!*/ Body;

+    [ContractInvariantMethod]

+    void ObjectInvariant() {

+      Contract.Invariant(Body != null);

+    }

+

+    public MatchCaseExpr(IToken tok, string id, [Captured] List<BoundVar/*!*/>/*!*/ arguments, Expression body)

+      : base(tok, id, arguments)

+    {

+      Contract.Requires(tok != null);

+      Contract.Requires(id != null);

+      Contract.Requires(cce.NonNullElements(arguments));

+      Contract.Requires(body != null);

       this.Body = body;

     }

   }

diff --git a/Dafny/Parser.cs b/Dafny/Parser.cs
index 1837ea9e..290609fc 100644
--- a/Dafny/Parser.cs
+++ b/Dafny/Parser.cs
@@ -20,7 +20,7 @@ public class Parser {
 	public const int _digits = 2;

 	public const int _arrayToken = 3;

 	public const int _string = 4;

-	public const int maxT = 103;

+	public const int maxT = 104;

 

 	const bool T = true;

 	const bool x = false;

@@ -402,7 +402,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			mm.Add(m); 

 		} else if (la.kind == 18) {

 			CouplingInvDecl(mmod, mm);

-		} else SynErr(104);

+		} else SynErr(105);

 	}

 

 	void GenericParameters(List<TypeParameter/*!*/>/*!*/ typeArgs) {

@@ -486,7 +486,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			}

 			FunctionBody(out bb, out bodyStart, out bodyEnd);

 			body = bb; 

-		} else SynErr(105);

+		} else SynErr(106);

 		parseVarScope.PopMarker();

 		f = new Function(id, id.val, mmod.IsStatic, !isFunctionMethod, mmod.IsUnlimited, typeArgs, formals, returnType, reqs, reads, ens, decreases, body, attrs);

 		f.BodyStartTok = bodyStart;

@@ -515,7 +515,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		} else if (la.kind == 10) {

 			Get();

 			isRefinement = true; 

-		} else SynErr(106);

+		} else SynErr(107);

 		if (mmod.IsUnlimited) { SemErr(t, "methods cannot be declared 'unlimited'"); }

 		

 		while (la.kind == 7) {

@@ -542,7 +542,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			}

 			BlockStmt(out bb, out bodyStart, out bodyEnd);

 			body = (BlockStmt)bb; 

-		} else SynErr(107);

+		} else SynErr(108);

 		parseVarScope.PopMarker();

 		if (isRefinement)

 		  m = new MethodRefinement(id, id.val, mmod.IsStatic, mmod.IsGhost, typeArgs, ins, outs, req, mod, ens, dec, body, attrs);

@@ -645,7 +645,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			e = new ITEExpr(x, e, e0, e1); 

 		} else if (StartOf(8)) {

 			EquivExpression(out e);

-		} else SynErr(108);

+		} else SynErr(109);

 	}

 

 	void GIdentType(bool allowGhost, out IToken/*!*/ id, out Type/*!*/ ty, out bool isGhost) {

@@ -735,7 +735,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			

 		} else if (la.kind == 1 || la.kind == 3 || la.kind == 36) {

 			ReferenceType(out tok, out ty);

-		} else SynErr(109);

+		} else SynErr(110);

 	}

 

 	void Formals(bool incoming, bool allowGhosts, List<Formal/*!*/>/*!*/ formals) {

@@ -785,12 +785,12 @@ List<Expression/*!*/>/*!*/ decreases) {
 				Expression(out e);

 				Expect(15);

 				ens.Add(new MaybeFreeExpression(e, isFree)); 

-			} else SynErr(110);

+			} else SynErr(111);

 		} else if (la.kind == 29) {

 			Get();

 			Expressions(decreases);

 			Expect(15);

-		} else SynErr(111);

+		} else SynErr(112);

 	}

 

 	void BlockStmt(out Statement/*!*/ block, out IToken bodyStart, out IToken bodyEnd) {

@@ -872,7 +872,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 				GenericInstantiation(gt);

 			}

 			ty = new UserDefinedType(tok, tok.val, gt); 

-		} else SynErr(112);

+		} else SynErr(113);

 	}

 

 	void FunctionSpec(List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ ens, List<Expression/*!*/>/*!*/ decreases) {

@@ -904,7 +904,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Get();

 			Expressions(decreases);

 			Expect(15);

-		} else SynErr(113);

+		} else SynErr(114);

 	}

 

 	void FunctionBody(out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd) {

@@ -915,7 +915,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			MatchExpression(out e);

 		} else if (StartOf(9)) {

 			Expression(out e);

-		} else SynErr(114);

+		} else SynErr(115);

 		Expect(8);

 		bodyEnd = t; 

 	}

@@ -927,7 +927,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			fe = new FrameExpression(new WildcardExpr(t), null); 

 		} else if (StartOf(9)) {

 			FrameExpression(out fe);

-		} else SynErr(115);

+		} else SynErr(116);

 	}

 

 	void PossiblyWildExpression(out Expression/*!*/ e) {

@@ -938,7 +938,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			e = new WildcardExpr(t); 

 		} else if (StartOf(9)) {

 			Expression(out e);

-		} else SynErr(116);

+		} else SynErr(117);

 	}

 

 	void MatchExpression(out Expression/*!*/ e) {

@@ -995,7 +995,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			ss.Add(s); 

 		} else if (la.kind == 11 || la.kind == 16) {

 			VarDeclStmts(ss);

-		} else SynErr(117);

+		} else SynErr(118);

 	}

 

 	void OneStmt(out Statement/*!*/ s) {

@@ -1019,7 +1019,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			PrintStmt(out s);

 			break;

 		}

-		case 1: case 30: case 95: case 96: {

+		case 1: case 30: case 96: case 97: {

 			AssignStmt(out s);

 			break;

 		}

@@ -1073,7 +1073,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			s = new ReturnStmt(x); 

 			break;

 		}

-		default: SynErr(118); break;

+		default: SynErr(119); break;

 		}

 	}

 

@@ -1246,7 +1246,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			} else if (la.kind == 7) {

 				BlockStmt(out s, out bodyStart, out bodyEnd);

 				els = s; 

-			} else SynErr(119);

+			} else SynErr(120);

 		}

 		ifStmt = new IfStmt(x, guard, thn, els); 

 	}

@@ -1354,7 +1354,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		} else if (la.kind == 51) {

 			HavocStmt(out s);

 			if (s is AssignStmt) { bodyAssign = (AssignStmt)s; } 

-		} else SynErr(120);

+		} else SynErr(121);

 		Expect(8);

 		if (bodyAssign != null) {

 		 s = new ForeachStmt(x, new BoundVar(boundVar, boundVar.val, ty), collection, range, bodyPrefix, bodyAssign);

@@ -1393,7 +1393,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		} else if (StartOf(9)) {

 			Expression(out e);

 			ee = new List<Expression>(); ee.Add(e); 

-		} else SynErr(121);

+		} else SynErr(122);

 		if (ee == null && ty == null) { ee = new List<Expression>(); ee.Add(dummyExpr); } 

 	}

 

@@ -1401,9 +1401,9 @@ List<Expression/*!*/>/*!*/ decreases) {
 		Contract.Ensures(Contract.ValueAtReturn(out e) != null); e = dummyExpr; 

 		if (la.kind == 1) {

 			IdentOrFuncExpression(out e);

-		} else if (la.kind == 30 || la.kind == 95 || la.kind == 96) {

+		} else if (la.kind == 30 || la.kind == 96 || la.kind == 97) {

 			ObjectExpression(out e);

-		} else SynErr(122);

+		} else SynErr(123);

 		while (la.kind == 49 || la.kind == 92) {

 			SelectOrCallSuffix(ref e);

 		}

@@ -1449,7 +1449,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		} else if (StartOf(9)) {

 			Expression(out ee);

 			e = ee; 

-		} else SynErr(123);

+		} else SynErr(124);

 		Expect(31);

 	}

 

@@ -1489,10 +1489,10 @@ List<Expression/*!*/>/*!*/ decreases) {
 		Contract.Ensures(Contract.ValueAtReturn(out e) != null); e = dummyExpr; 

 		if (la.kind == 1) {

 			IdentOrFuncExpression(out e);

-		} else if (la.kind == 30 || la.kind == 95 || la.kind == 96) {

+		} else if (la.kind == 30 || la.kind == 96 || la.kind == 97) {

 			ObjectExpression(out e);

 			SelectOrCallSuffix(ref e);

-		} else SynErr(124);

+		} else SynErr(125);

 		while (la.kind == 49 || la.kind == 92) {

 			SelectOrCallSuffix(ref e);

 		}

@@ -1506,7 +1506,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		} else if (StartOf(9)) {

 			Expression(out e);

 			arg = new Attributes.Argument(e); 

-		} else SynErr(125);

+		} else SynErr(126);

 	}

 

 	void EquivExpression(out Expression/*!*/ e0) {

@@ -1536,7 +1536,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Get();

 		} else if (la.kind == 66) {

 			Get();

-		} else SynErr(126);

+		} else SynErr(127);

 	}

 

 	void LogicalExpression(out Expression/*!*/ e0) {

@@ -1574,7 +1574,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Get();

 		} else if (la.kind == 68) {

 			Get();

-		} else SynErr(127);

+		} else SynErr(128);

 	}

 

 	void RelationalExpression(out Expression/*!*/ e0) {

@@ -1592,7 +1592,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Get();

 		} else if (la.kind == 70) {

 			Get();

-		} else SynErr(128);

+		} else SynErr(129);

 	}

 

 	void OrOp() {

@@ -1600,7 +1600,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Get();

 		} else if (la.kind == 72) {

 			Get();

-		} else SynErr(129);

+		} else SynErr(130);

 	}

 

 	void Term(out Expression/*!*/ e0) {

@@ -1676,7 +1676,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			x = t;  op = BinaryExpr.Opcode.Ge; 

 			break;

 		}

-		default: SynErr(130); break;

+		default: SynErr(131); break;

 		}

 	}

 

@@ -1698,7 +1698,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		} else if (la.kind == 83) {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Sub; 

-		} else SynErr(131);

+		} else SynErr(132);

 	}

 

 	void UnaryExpression(out Expression/*!*/ e) {

@@ -1717,7 +1717,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			SelectExpression(out e);

 		} else if (StartOf(16)) {

 			ConstAtomExpression(out e);

-		} else SynErr(132);

+		} else SynErr(133);

 	}

 

 	void MulOp(out IToken/*!*/ x, out BinaryExpr.Opcode op) {

@@ -1731,7 +1731,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		} else if (la.kind == 85) {

 			Get();

 			x = t;  op = BinaryExpr.Opcode.Mod; 

-		} else SynErr(133);

+		} else SynErr(134);

 	}

 

 	void NegOp() {

@@ -1739,7 +1739,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Get();

 		} else if (la.kind == 87) {

 			Get();

-		} else SynErr(134);

+		} else SynErr(135);

 	}

 

 	void ConstAtomExpression(out Expression/*!*/ e) {

@@ -1793,6 +1793,15 @@ List<Expression/*!*/>/*!*/ decreases) {
 			e = new FreshExpr(x, e); 

 			break;

 		}

+		case 94: {

+			Get();

+			x = t; 

+			Expect(30);

+			Expression(out e);

+			Expect(31);

+			e = new AllocatedExpr(x, e); 

+			break;

+		}

 		case 59: {

 			Get();

 			x = t; 

@@ -1821,7 +1830,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Expect(50);

 			break;

 		}

-		default: SynErr(135); break;

+		default: SynErr(136); break;

 		}

 	}

 

@@ -1860,10 +1869,10 @@ List<Expression/*!*/>/*!*/ decreases) {
 

 	void ObjectExpression(out Expression/*!*/ e) {

 		Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;  e = dummyExpr; 

-		if (la.kind == 95) {

+		if (la.kind == 96) {

 			Get();

 			e = new ThisExpr(t); 

-		} else if (la.kind == 96) {

+		} else if (la.kind == 97) {

 			Get();

 			x = t; 

 			Expect(30);

@@ -1876,9 +1885,9 @@ List<Expression/*!*/>/*!*/ decreases) {
 				QuantifierGuts(out e);

 			} else if (StartOf(9)) {

 				Expression(out e);

-			} else SynErr(136);

+			} else SynErr(137);

 			Expect(31);

-		} else SynErr(137);

+		} else SynErr(138);

 	}

 

 	void SelectOrCallSuffix(ref Expression/*!*/ e) {

@@ -1906,7 +1915,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			if (StartOf(9)) {

 				Expression(out ee);

 				e0 = ee; 

-				if (la.kind == 94) {

+				if (la.kind == 95) {

 					Get();

 					anyDots = true; 

 					if (StartOf(9)) {

@@ -1928,12 +1937,12 @@ List<Expression/*!*/>/*!*/ decreases) {
 						multipleIndices.Add(ee);

 						

 					}

-				} else SynErr(138);

-			} else if (la.kind == 94) {

+				} else SynErr(139);

+			} else if (la.kind == 95) {

 				Get();

 				Expression(out ee);

 				anyDots = true;  e1 = ee; 

-			} else SynErr(139);

+			} else SynErr(140);

 			if (multipleIndices != null) {

 			 e = new MultiSelectExpr(x, e, multipleIndices);

 			} else {

@@ -1955,7 +1964,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			}

 			

 			Expect(50);

-		} else SynErr(140);

+		} else SynErr(141);

 	}

 

 	void QuantifierGuts(out Expression/*!*/ q) {

@@ -1967,13 +1976,13 @@ List<Expression/*!*/>/*!*/ decreases) {
 		Triggers trigs = null;

 		Expression/*!*/ body;

 		

-		if (la.kind == 97 || la.kind == 98) {

+		if (la.kind == 98 || la.kind == 99) {

 			Forall();

 			x = t;  univ = true; 

-		} else if (la.kind == 99 || la.kind == 100) {

+		} else if (la.kind == 100 || la.kind == 101) {

 			Exists();

 			x = t; 

-		} else SynErr(141);

+		} else SynErr(142);

 		parseVarScope.PushMarker(); 

 		IdentTypeOptional(out bv);

 		bvars.Add(bv);  parseVarScope.Push(bv.Name, bv.Name); 

@@ -1997,19 +2006,19 @@ List<Expression/*!*/>/*!*/ decreases) {
 	}

 

 	void Forall() {

-		if (la.kind == 97) {

+		if (la.kind == 98) {

 			Get();

-		} else if (la.kind == 98) {

+		} else if (la.kind == 99) {

 			Get();

-		} else SynErr(142);

+		} else SynErr(143);

 	}

 

 	void Exists() {

-		if (la.kind == 99) {

+		if (la.kind == 100) {

 			Get();

-		} else if (la.kind == 100) {

+		} else if (la.kind == 101) {

 			Get();

-		} else SynErr(143);

+		} else SynErr(144);

 	}

 

 	void AttributeOrTrigger(ref Attributes attrs, ref Triggers trigs) {

@@ -2022,16 +2031,16 @@ List<Expression/*!*/>/*!*/ decreases) {
 			es = new List<Expression/*!*/>(); 

 			Expressions(es);

 			trigs = new Triggers(es, trigs); 

-		} else SynErr(144);

+		} else SynErr(145);

 		Expect(8);

 	}

 

 	void QSep() {

-		if (la.kind == 101) {

+		if (la.kind == 102) {

 			Get();

-		} else if (la.kind == 102) {

+		} else if (la.kind == 103) {

 			Get();

-		} else SynErr(145);

+		} else SynErr(146);

 	}

 

 	void AttributeBody(ref Attributes attrs) {

@@ -2066,25 +2075,25 @@ List<Expression/*!*/>/*!*/ decreases) {
 	}

 	

 	static readonly bool[,]/*!*/ set = {

-		{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

-		{x,x,x,x, x,T,x,x, x,T,T,T, T,T,T,x, T,x,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

-		{x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, T,x,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

-		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

-		{x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

-		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

-		{x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

-		{x,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

-		{x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,T,T,T, x,T,x,T, T,x,x,x, x,x,x,x, x},

-		{x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,T,T,T, x,T,x,T, T,x,x,x, x,x,x,x, x},

-		{x,T,x,x, x,x,x,T, x,x,x,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,x, x,x,x,T, T,x,T,x, T,T,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x},

-		{x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,T,x,x, T,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,T,T,T, x,T,x,T, T,x,x,x, x,x,x,x, x},

-		{x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,x, x,x,x,T, T,x,T,x, T,T,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x},

-		{x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x},

-		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

-		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x},

-		{x,x,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,T,x,x, x,x,x,x, x,x,x,x, x},

-		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,x,x, x},

-		{x,T,T,x, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,T,T,T, x,T,x,T, T,x,x,x, x,x,x,x, x}

+		{T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

+		{x,x,x,x, x,T,x,x, x,T,T,T, T,T,T,x, T,x,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

+		{x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, T,x,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

+		{x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

+		{x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

+		{x,T,x,T, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

+		{x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,T,T,T, x,T,T,x, T,T,x,x, x,x,x,x, x,x},

+		{x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,T,T,T, x,T,T,x, T,T,x,x, x,x,x,x, x,x},

+		{x,T,x,x, x,x,x,T, x,x,x,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,x, x,x,x,T, T,x,T,x, T,T,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x},

+		{x,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,T,x,x, T,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,T,T,T, x,T,T,x, T,T,x,x, x,x,x,x, x,x},

+		{x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,x, x,x,x,T, T,x,T,x, T,T,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x},

+		{x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,x,x, x,x,x,x, x,x},

+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},

+		{x,x,T,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,T,T,x, x,x,x,x, x,x,x,x, x,x},

+		{x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x},

+		{x,T,T,x, T,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,T,T,T, x,T,T,x, T,T,x,x, x,x,x,x, x,x}

 

 	};

 } // end Parser

@@ -2201,58 +2210,59 @@ public class Errors {
 			case 91: s = "\"#\" expected"; break;

 			case 92: s = "\".\" expected"; break;

 			case 93: s = "\"fresh\" expected"; break;

-			case 94: s = "\"..\" expected"; break;

-			case 95: s = "\"this\" expected"; break;

-			case 96: s = "\"old\" expected"; break;

-			case 97: s = "\"forall\" expected"; break;

-			case 98: s = "\"\\u2200\" expected"; break;

-			case 99: s = "\"exists\" expected"; break;

-			case 100: s = "\"\\u2203\" expected"; break;

-			case 101: s = "\"::\" expected"; break;

-			case 102: s = "\"\\u2022\" expected"; break;

-			case 103: s = "??? expected"; break;

-			case 104: s = "invalid ClassMemberDecl"; break;

-			case 105: s = "invalid FunctionDecl"; break;

-			case 106: s = "invalid MethodDecl"; break;

+			case 94: s = "\"allocated\" expected"; break;

+			case 95: s = "\"..\" expected"; break;

+			case 96: s = "\"this\" expected"; break;

+			case 97: s = "\"old\" expected"; break;

+			case 98: s = "\"forall\" expected"; break;

+			case 99: s = "\"\\u2200\" expected"; break;

+			case 100: s = "\"exists\" expected"; break;

+			case 101: s = "\"\\u2203\" expected"; break;

+			case 102: s = "\"::\" expected"; break;

+			case 103: s = "\"\\u2022\" expected"; break;

+			case 104: s = "??? expected"; break;

+			case 105: s = "invalid ClassMemberDecl"; break;

+			case 106: s = "invalid FunctionDecl"; break;

 			case 107: s = "invalid MethodDecl"; break;

-			case 108: s = "invalid Expression"; break;

-			case 109: s = "invalid TypeAndToken"; break;

-			case 110: s = "invalid MethodSpec"; break;

+			case 108: s = "invalid MethodDecl"; break;

+			case 109: s = "invalid Expression"; break;

+			case 110: s = "invalid TypeAndToken"; break;

 			case 111: s = "invalid MethodSpec"; break;

-			case 112: s = "invalid ReferenceType"; break;

-			case 113: s = "invalid FunctionSpec"; break;

-			case 114: s = "invalid FunctionBody"; break;

-			case 115: s = "invalid PossiblyWildFrameExpression"; break;

-			case 116: s = "invalid PossiblyWildExpression"; break;

-			case 117: s = "invalid Stmt"; break;

-			case 118: s = "invalid OneStmt"; break;

-			case 119: s = "invalid IfStmt"; break;

-			case 120: s = "invalid ForeachStmt"; break;

-			case 121: s = "invalid AssignRhs"; break;

-			case 122: s = "invalid SelectExpression"; break;

-			case 123: s = "invalid Guard"; break;

-			case 124: s = "invalid CallStmtSubExpr"; break;

-			case 125: s = "invalid AttributeArg"; break;

-			case 126: s = "invalid EquivOp"; break;

-			case 127: s = "invalid ImpliesOp"; break;

-			case 128: s = "invalid AndOp"; break;

-			case 129: s = "invalid OrOp"; break;

-			case 130: s = "invalid RelOp"; break;

-			case 131: s = "invalid AddOp"; break;

-			case 132: s = "invalid UnaryExpression"; break;

-			case 133: s = "invalid MulOp"; break;

-			case 134: s = "invalid NegOp"; break;

-			case 135: s = "invalid ConstAtomExpression"; break;

-			case 136: s = "invalid ObjectExpression"; break;

+			case 112: s = "invalid MethodSpec"; break;

+			case 113: s = "invalid ReferenceType"; break;

+			case 114: s = "invalid FunctionSpec"; break;

+			case 115: s = "invalid FunctionBody"; break;

+			case 116: s = "invalid PossiblyWildFrameExpression"; break;

+			case 117: s = "invalid PossiblyWildExpression"; break;

+			case 118: s = "invalid Stmt"; break;

+			case 119: s = "invalid OneStmt"; break;

+			case 120: s = "invalid IfStmt"; break;

+			case 121: s = "invalid ForeachStmt"; break;

+			case 122: s = "invalid AssignRhs"; break;

+			case 123: s = "invalid SelectExpression"; break;

+			case 124: s = "invalid Guard"; break;

+			case 125: s = "invalid CallStmtSubExpr"; break;

+			case 126: s = "invalid AttributeArg"; break;

+			case 127: s = "invalid EquivOp"; break;

+			case 128: s = "invalid ImpliesOp"; break;

+			case 129: s = "invalid AndOp"; break;

+			case 130: s = "invalid OrOp"; break;

+			case 131: s = "invalid RelOp"; break;

+			case 132: s = "invalid AddOp"; break;

+			case 133: s = "invalid UnaryExpression"; break;

+			case 134: s = "invalid MulOp"; break;

+			case 135: s = "invalid NegOp"; break;

+			case 136: s = "invalid ConstAtomExpression"; break;

 			case 137: s = "invalid ObjectExpression"; break;

-			case 138: s = "invalid SelectOrCallSuffix"; break;

+			case 138: s = "invalid ObjectExpression"; break;

 			case 139: s = "invalid SelectOrCallSuffix"; break;

 			case 140: s = "invalid SelectOrCallSuffix"; break;

-			case 141: s = "invalid QuantifierGuts"; break;

-			case 142: s = "invalid Forall"; break;

-			case 143: s = "invalid Exists"; break;

-			case 144: s = "invalid AttributeOrTrigger"; break;

-			case 145: s = "invalid QSep"; break;

+			case 141: s = "invalid SelectOrCallSuffix"; break;

+			case 142: s = "invalid QuantifierGuts"; break;

+			case 143: s = "invalid Forall"; break;

+			case 144: s = "invalid Exists"; break;

+			case 145: s = "invalid AttributeOrTrigger"; break;

+			case 146: s = "invalid QSep"; break;

 

 			default: s = "error " + n; break;

 		}

diff --git a/Dafny/Printer.cs b/Dafny/Printer.cs
index dd4c7be5..0b93a1dc 100644
--- a/Dafny/Printer.cs
+++ b/Dafny/Printer.cs
@@ -101,7 +101,7 @@ namespace Microsoft.Dafny {
     public void PrintClass_Members(ClassDecl c, int indent)

     {

       Contract.Requires(c != null);

-      Contract.Requires(c.Members.Count != 0);

+      Contract.Requires( c.Members.Count != 0);

     

       int state = 0;  // 0 - no members yet; 1 - previous member was a field; 2 - previous member was non-field

       foreach (MemberDecl m in c.Members) {

@@ -184,7 +184,7 @@ namespace Microsoft.Dafny {
         if (arg.S != null) {

           wr.Write("\"{0}\"", arg.S);

         } else {

-          Contract.Assert(arg.E != null);

+          Contract.Assert( arg.E != null);

           PrintExpression(arg.E);

         }

       }

@@ -260,7 +260,7 @@ namespace Microsoft.Dafny {
     const int IndentAmount = 2;

     const string BunchaSpaces = "                                ";

     void Indent(int amount)

-    {  Contract.Requires(0 <= amount);

+    {  Contract.Requires( 0 <= amount);

     

       while (0 < amount) {

         wr.Write(BunchaSpaces.Substring(0, amount));

@@ -667,7 +667,7 @@ namespace Microsoft.Dafny {
     /// </summary>

     void PrintExpr(Expression expr, int contextBindingStrength, bool fragileContext, int indent)

     {

-      Contract.Requires(-1 <= indent);

+      Contract.Requires( -1 <= indent);

     

       Contract.Requires(expr != null);

       if (expr is LiteralExpr) {

@@ -728,7 +728,7 @@ namespace Microsoft.Dafny {
         PrintExpr(e.Seq, 0x00, false, indent);  // BOGUS: fix me

         wr.Write("[");

         if (e.SelectOne) {

-          Contract.Assert(e.E0 != null);

+          Contract.Assert( e.E0 != null);

           PrintExpression(e.E0);

         } else {

           if (e.E0 != null) {

@@ -805,7 +805,12 @@ namespace Microsoft.Dafny {
         wr.Write("fresh(");

         PrintExpression(((FreshExpr)expr).E);

         wr.Write(")");

-      

+

+      } else if (expr is AllocatedExpr) {

+        wr.Write("allocated(");

+        PrintExpression(((AllocatedExpr)expr).E);

+        wr.Write(")");

+

       } else if (expr is UnaryExpr) {

         UnaryExpr e = (UnaryExpr)expr;

         if (e.Op == UnaryExpr.Opcode.SeqLength) {

diff --git a/Dafny/Resolver.cs b/Dafny/Resolver.cs
index 6c062820..080930ea 100644
--- a/Dafny/Resolver.cs
+++ b/Dafny/Resolver.cs
@@ -1992,7 +1992,13 @@ namespace Microsoft.Dafny {
           Error(expr, "the argument of a fresh expression must denote an object or a collection of objects (instead got {0})", e.E.Type);

         }

         expr.Type = Type.Bool;

-        

+

+      } else if (expr is AllocatedExpr) {

+        AllocatedExpr e = (AllocatedExpr)expr;

+        ResolveExpression(e.E, twoState, specContext);

+        // e.E can be of any type

+        expr.Type = Type.Bool;

+

       } else if (expr is UnaryExpr) {

         UnaryExpr e = (UnaryExpr)expr;

         ResolveExpression(e.E, twoState, specContext);

@@ -2479,8 +2485,9 @@ namespace Microsoft.Dafny {
         OldExpr e = (OldExpr)expr;

         return UsesSpecFeatures(e.E);

       } else if (expr is FreshExpr) {

-        FreshExpr e = (FreshExpr)expr;

-        return UsesSpecFeatures(e.E);

+        return true;

+      } else if (expr is AllocatedExpr) {

+        return true;

       } else if (expr is UnaryExpr) {

         UnaryExpr e = (UnaryExpr)expr;

         return UsesSpecFeatures(e.E);

diff --git a/Dafny/Scanner.cs b/Dafny/Scanner.cs
index de87c6ad..b7e7f57b 100644
--- a/Dafny/Scanner.cs
+++ b/Dafny/Scanner.cs
@@ -209,8 +209,8 @@ public class UTF8Buffer: Buffer {
 public class Scanner {

 	const char EOL = '\n';

 	const int eofSym = 0; /* pdt */

-	const int maxT = 103;

-	const int noSym = 103;

+	const int maxT = 104;

+	const int noSym = 104;

 

 

 [ContractInvariantMethod]

@@ -535,10 +535,11 @@ void objectInvariant(){
 			case "true": t.kind = 89; break;

 			case "null": t.kind = 90; break;

 			case "fresh": t.kind = 93; break;

-			case "this": t.kind = 95; break;

-			case "old": t.kind = 96; break;

-			case "forall": t.kind = 97; break;

-			case "exists": t.kind = 99; break;

+			case "allocated": t.kind = 94; break;

+			case "this": t.kind = 96; break;

+			case "old": t.kind = 97; break;

+			case "forall": t.kind = 98; break;

+			case "exists": t.kind = 100; break;

 			default: break;

 		}

 	}

@@ -712,15 +713,15 @@ void objectInvariant(){
 			case 52:

 				{t.kind = 91; break;}

 			case 53:

-				{t.kind = 94; break;}

+				{t.kind = 95; break;}

 			case 54:

-				{t.kind = 98; break;}

+				{t.kind = 99; break;}

 			case 55:

-				{t.kind = 100; break;}

-			case 56:

 				{t.kind = 101; break;}

-			case 57:

+			case 56:

 				{t.kind = 102; break;}

+			case 57:

+				{t.kind = 103; break;}

 			case 58:

 				recEnd = pos; recKind = 20;

 				if (ch == '=') {AddCh(); goto case 26;}

diff --git a/Dafny/Translator.cs b/Dafny/Translator.cs
index 0a96a197..181ec9ec 100644
--- a/Dafny/Translator.cs
+++ b/Dafny/Translator.cs
@@ -278,6 +278,7 @@ namespace Microsoft.Dafny {
     {

       Contract.Requires(dt != null);

       Contract.Requires(sink != null && predef != null);

+      sink.TopLevelDeclarations.Add(GetClass(dt));

     

       foreach (DatatypeCtor ctor in dt.Ctors) {

         // Add:  function #dt.ctor(paramTypes) returns (DatatypeType);

@@ -289,12 +290,24 @@ namespace Microsoft.Dafny {
         Bpl.Variable resType = new Bpl.Formal(ctor.tok, new Bpl.TypedIdent(ctor.tok, Bpl.TypedIdent.NoName, predef.DatatypeType), false);

         Bpl.Function fn = new Bpl.Function(ctor.tok, ctor.FullName, argTypes, resType);

         sink.TopLevelDeclarations.Add(fn);

+

+        // Add:  axiom (forall params :: #dt.ctor(params)-has-the-expected-type);

+        Bpl.VariableSeq bvs;

+        List<Bpl.Expr> args;

+        CreateBoundVariables(ctor.Formals, out bvs, out args);

+        Bpl.Expr ct = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);

+        List<Type> tpArgs = new List<Type>();  // we use an empty list of type arguments, because we don't want Good_Datatype to produce any DtTypeParams predicates anyway

+        Bpl.Expr wh = new ExpressionTranslator(this, predef, ctor.tok).Good_Datatype(ctor.tok, ct, dt, tpArgs);

+        if (bvs.Length != 0) {

+          wh = new Bpl.ForallExpr(ctor.tok, bvs, wh);

+        }

+        sink.TopLevelDeclarations.Add(new Bpl.Axiom(ctor.tok, wh));

+

         // Add:  const unique ##dt.ctor: DtCtorId;

         Bpl.Constant cid = new Bpl.Constant(ctor.tok, new Bpl.TypedIdent(ctor.tok, "#" + ctor.FullName, predef.DtCtorId), true);

         sink.TopLevelDeclarations.Add(cid);

+

         // Add:  axiom (forall params :: DatatypeCtorId(#dt.ctor(params)) == ##dt.ctor);

-        Bpl.VariableSeq bvs;

-        List<Bpl.Expr> args;

         CreateBoundVariables(ctor.Formals, out bvs, out args);

         Bpl.Expr lhs = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);

         lhs = FunctionCall(ctor.tok, BuiltinFunction.DatatypeCtorId, null, lhs);

@@ -303,9 +316,35 @@ namespace Microsoft.Dafny {
           q = new Bpl.ForallExpr(ctor.tok, bvs, q);

         }

         sink.TopLevelDeclarations.Add(new Bpl.Axiom(ctor.tok, q));

-        // Add injectivity axioms:

+

+        // Add:  axiom (forall params, h: HeapType :: 

+        //                 { DtAlloc(#dt.ctor(params), h) }

+        //                 $IsGoodHeap(h) ==>

+        //                     (DtAlloc(#dt.ctor(params), h) <==> ...each param has its expected type...));

+        CreateBoundVariables(ctor.Formals, out bvs, out args);

+        lhs = FunctionCall(ctor.tok, ctor.FullName, predef.DatatypeType, args);

+        Bpl.BoundVariable hVar = new Bpl.BoundVariable(ctor.tok, new Bpl.TypedIdent(ctor.tok, "$h", predef.HeapType));

+        Bpl.Expr h = new Bpl.IdentifierExpr(ctor.tok, hVar);

+        bvs.Add(hVar); args.Add(h);

+        ExpressionTranslator etranH = new ExpressionTranslator(this, predef, h);

+        Bpl.Expr isGoodHeap = FunctionCall(ctor.tok, BuiltinFunction.IsGoodHeap, null, h);

+        lhs = FunctionCall(ctor.tok, BuiltinFunction.DtAlloc, null, lhs, h);

+        Bpl.Expr pt = Bpl.Expr.True;

         int i = 0;

         foreach (Formal arg in ctor.Formals) {

+          Bpl.Expr whp = GetWhereClause(arg.tok, args[i], arg.Type, etranH);

+          if (whp != null) {

+            pt = BplAnd(pt, whp);

+          }

+          i++;

+        }

+        Bpl.Trigger tr = new Bpl.Trigger(ctor.tok, true, new ExprSeq(lhs));

+        q = new Bpl.ForallExpr(ctor.tok, bvs, tr, Bpl.Expr.Imp(isGoodHeap, Bpl.Expr.Iff(lhs, pt)));

+        sink.TopLevelDeclarations.Add(new Bpl.Axiom(ctor.tok, q));

+

+        // Add injectivity axioms:

+        i = 0;

+        foreach (Formal arg in ctor.Formals) {

           // function ##dt.ctor#i(DatatypeType) returns (Ti);

           argTypes = new Bpl.VariableSeq();

           argTypes.Add(new Bpl.Formal(ctor.tok, new Bpl.TypedIdent(ctor.tok, Bpl.TypedIdent.NoName, predef.DatatypeType), true));

@@ -399,32 +438,28 @@ namespace Microsoft.Dafny {
             Bpl.Function ff = GetReadonlyField(f);

             sink.TopLevelDeclarations.Add(ff);

           }

-          

+

           AddAllocationAxiom(f);

           

         } else if (member is Function) {

           Function f = (Function)member;

           AddFunction(f);

-          if (f.Body != null || f.Ens.Count != 0) {

-            if (f.Body is MatchExpr) {

-              MatchExpr me = (MatchExpr)f.Body;

-              Formal formal = (Formal)((IdentifierExpr)me.Source).Var;  // correctness of casts follows from what resolution checks

-              foreach (MatchCaseExpr mc in me.Cases) {

-                Contract.Assert(mc.Ctor != null);  // the field is filled in by resolution

-                Bpl.Axiom ax = FunctionAxiom(f, mc.Body, new List<Expression>(), formal, mc.Ctor, mc.Arguments);

-                sink.TopLevelDeclarations.Add(ax);

-              }

-              if (f.Ens.Count != 0) {

-                Bpl.Axiom ax = FunctionAxiom(f, null, f.Ens, null, null, null);

-                sink.TopLevelDeclarations.Add(ax);

-              }

-            } else {

-              Bpl.Axiom ax = FunctionAxiom(f, f.Body, f.Ens, null, null, null);

+          if (f.Body is MatchExpr) {

+            MatchExpr me = (MatchExpr)f.Body;

+            Formal formal = (Formal)((IdentifierExpr)me.Source).Var;  // correctness of casts follows from what resolution checks

+            foreach (MatchCaseExpr mc in me.Cases) {

+              Contract.Assert(mc.Ctor != null);  // the field is filled in by resolution

+              Bpl.Axiom ax = FunctionAxiom(f, mc.Body, new List<Expression>(), formal, mc.Ctor, mc.Arguments);

               sink.TopLevelDeclarations.Add(ax);

             }

-            if (f.IsRecursive && !f.IsUnlimited) {

-              AddLimitedAxioms(f);

-            }

+            Bpl.Axiom axPost = FunctionAxiom(f, null, f.Ens, null, null, null);

+            sink.TopLevelDeclarations.Add(axPost);

+          } else {

+            Bpl.Axiom ax = FunctionAxiom(f, f.Body, f.Ens, null, null, null);

+            sink.TopLevelDeclarations.Add(ax);

+          }

+          if (f.IsRecursive && !f.IsUnlimited) {

+            AddLimitedAxioms(f);

           }

           AddFrameAxiom(f);

           AddWellformednessCheck(f);

@@ -477,11 +512,15 @@ namespace Microsoft.Dafny {
       //   ==>

       //   (forall $Heap, formals ::

       //       { f(args) }

-      //       $IsHeap($Heap) && this != null &&

-      //       (((mh != ModuleContextHeight || fh != FunctionContextHeight || InMethodContext) && Pre($Heap,args)) ||

-      //        f#canCall(args))

+      //       f#canCall(args) ||

+      //       ( (mh != ModuleContextHeight || fh != FunctionContextHeight || InMethodContext) &&

+      //         $IsHeap($Heap) && this != null && formals-have-the-expected-types &&

+      //         Pre($Heap,args))

       //       ==>

-      //       f(args) == body && ens);

+      //       body-can-make-its-calls &&

+      //       f(args) == body &&

+      //       ens &&

+      //       f(args)-has-the-expected-type);

       //

       // The variables "formals" are the formals of function "f"; except, if a specialization is provided, then

       // "specializationFormal" (which is expected to be among the formals of "f") is excluded and replaced by

@@ -503,6 +542,9 @@ namespace Microsoft.Dafny {
       Bpl.BoundVariable bv = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, predef.HeapVarName, predef.HeapType));

       formals.Add(bv);

       args.Add(new Bpl.IdentifierExpr(f.tok, bv));

+      // ante:  $IsHeap($Heap) && this != null && formals-have-the-expected-types &&

+      Bpl.Expr ante = FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, etran.HeapExpr);

+      

       Bpl.BoundVariable bvThis;

       Bpl.Expr bvThisIdExpr;

       if (f.IsStatic) {

@@ -513,6 +555,12 @@ namespace Microsoft.Dafny {
         formals.Add(bvThis);

         bvThisIdExpr = new Bpl.IdentifierExpr(f.tok, bvThis);

         args.Add(bvThisIdExpr);

+        // add well-typedness conjunct to antecedent

+        Type thisType = Resolver.GetThisType(f.tok, cce.NonNull(f.EnclosingClass));

+        Bpl.Expr wh = Bpl.Expr.And(

+          Bpl.Expr.Neq(bvThisIdExpr, predef.Null),

+          etran.GoodRef(f.tok, bvThisIdExpr, thisType));

+        ante = Bpl.Expr.And(ante, wh);

       }

       DatatypeValue r = null;

       if (specializationReplacementFormals != null) {

@@ -524,6 +572,9 @@ namespace Microsoft.Dafny {
           IdentifierExpr ie = new IdentifierExpr(p.tok, p.UniqueName);

           ie.Var = p;  ie.Type = ie.Var.Type;  // resolve it here

           rArgs.Add(ie);

+          // add well-typedness conjunct to antecedent

+          Bpl.Expr wh = GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, bv), p.Type, etran);

+          if (wh != null) { ante = Bpl.Expr.And(ante, wh); }

         }

         r = new DatatypeValue(f.tok, cce.NonNull(ctor.EnclosingDatatype).Name, ctor.Name, rArgs);

         r.Ctor = ctor;  r.Type = new UserDefinedType(f.tok, ctor.EnclosingDatatype.Name, new List<Type>()/*this is not right, but it seems like it won't matter here*/);  // resolve it here

@@ -532,10 +583,15 @@ namespace Microsoft.Dafny {
         if (p != specializationFormal) {

           bv = new Bpl.BoundVariable(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, TrType(p.Type)));

           formals.Add(bv);

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

+          Bpl.Expr formal = new Bpl.IdentifierExpr(p.tok, bv);

+          args.Add(formal);

+          // add well-typedness conjunct to antecedent

+          Bpl.Expr wh = GetWhereClause(p.tok, formal, p.Type, etran);

+          if (wh != null) { ante = Bpl.Expr.And(ante, wh); }

         } else {

           Contract.Assert(r != null);  // it is set above

           args.Add(etran.TrExpr(r));

+          // note, well-typedness conjuncts for the replacement formals has already been done above

         }

       }

 

@@ -549,12 +605,6 @@ namespace Microsoft.Dafny {
             Bpl.Expr.Le(Bpl.Expr.Literal(mod.CallGraph.GetSCCRepresentativeId(f)), etran.FunctionContextHeight()),

             etran.InMethodContext())));

       

-      Bpl.Expr ante = FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, etran.HeapExpr);

-      if (!f.IsStatic) {

-        Contract.Assert(bvThisIdExpr != null);  // set to non-null value above when !f.IsStatic

-        ante = Bpl.Expr.And(ante, Bpl.Expr.Neq(bvThisIdExpr, predef.Null));

-      }

-

       Dictionary<IVariable, Expression> substMap = new Dictionary<IVariable, Expression>();

       if (specializationFormal != null) {

         Contract.Assert(r != null);

@@ -567,24 +617,27 @@ namespace Microsoft.Dafny {
       foreach (Expression req in f.Req) {

         pre = BplAnd(pre, etran.TrExpr(Substitute(req, null, substMap)));

       }

-      // useViaPre: (mh != ModuleContextHeight || fh != FunctionContextHeight || InMethodContext) && Pre

-      Bpl.Expr useViaPre =

-        Bpl.Expr.And(

-          Bpl.Expr.Or(Bpl.Expr.Or(

-            Bpl.Expr.Neq(Bpl.Expr.Literal(mod.Height), etran.ModuleContextHeight()),

-            Bpl.Expr.Neq(Bpl.Expr.Literal(mod.CallGraph.GetSCCRepresentativeId(f)), etran.FunctionContextHeight())),

-            etran.InMethodContext()),

-          pre);

+      // useViaContext: (mh != ModuleContextHeight || fh != FunctionContextHeight || InMethodContext)

+      Bpl.Expr useViaContext =

+        Bpl.Expr.Or(Bpl.Expr.Or(

+          Bpl.Expr.Neq(Bpl.Expr.Literal(mod.Height), etran.ModuleContextHeight()),

+          Bpl.Expr.Neq(Bpl.Expr.Literal(mod.CallGraph.GetSCCRepresentativeId(f)), etran.FunctionContextHeight())),

+          etran.InMethodContext());

       // useViaCanCall: f#canCall(args)

       Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(f.tok, f.FullName + "#canCall", Bpl.Type.Bool);

       Bpl.Expr useViaCanCall = new Bpl.NAryExpr(f.tok, new Bpl.FunctionCall(canCallFuncID), args);

-      ante = Bpl.Expr.And(ante, Bpl.Expr.Or(useViaPre, useViaCanCall));

+

+      // ante := useViaCanCall || (useViaContext && typeAnte && pre)

+      ante = Bpl.Expr.Or(useViaCanCall, BplAnd(useViaContext, BplAnd(ante, pre)));

 

       Bpl.Trigger tr = new Bpl.Trigger(f.tok, true, new Bpl.ExprSeq(funcAppl));

       Bpl.TypeVariableSeq typeParams = TrTypeParamDecls(f.TypeArgs);

       Bpl.Expr meat;

       if (body != null) {

-        meat = Bpl.Expr.Eq(funcAppl, etran.LimitedFunctions(f).TrExpr(Substitute(body, null, substMap)));

+        Expression bodyWithSubst = Substitute(body, null, substMap);

+        meat = Bpl.Expr.And(

+          CanCallAssumption(bodyWithSubst, etran),

+          Bpl.Expr.Eq(funcAppl, etran.LimitedFunctions(f).TrExpr(bodyWithSubst)));

       } else {

         meat = Bpl.Expr.True;

       }

@@ -592,8 +645,14 @@ namespace Microsoft.Dafny {
         Bpl.Expr q = etran.LimitedFunctions(f).TrExpr(Substitute(p, null, substMap));

         meat = BplAnd(meat, q);

       }

+      Bpl.Expr whr = GetWhereClause(f.tok, funcAppl, f.ResultType, etran);

+      if (whr != null) { meat = Bpl.Expr.And(meat, whr); }

       Bpl.Expr ax = new Bpl.ForallExpr(f.tok, typeParams, formals, null, tr, Bpl.Expr.Imp(ante, meat));

-      return new Bpl.Axiom(f.tok, Bpl.Expr.Imp(activate, ax));

+      string comment = "definition axiom for " + f.FullName;

+      if (specializationFormal != null) {

+        comment = string.Format("{0}, specialized for '{1}'", comment, specializationFormal.Name);

+      }

+      return new Bpl.Axiom(f.tok, Bpl.Expr.Imp(activate, ax), comment);

     }

     

     void AddLimitedAxioms(Function f){

@@ -636,15 +695,17 @@ namespace Microsoft.Dafny {
       sink.TopLevelDeclarations.Add(new Bpl.Axiom(f.tok, ax));

     }

     

+    /// <summary>

+    /// Generate:

+    ///   axiom (forall h: [ref, Field x]x, o: ref ::

+    ///        { h[o,f] }

+    ///        $IsGoodHeap(h) && o != null && h[o,alloc] ==> h[o,f]-has-the-expected-type);

+    /// </summary>

     void AddAllocationAxiom(Field f)

     {

       Contract.Requires(f != null);

       Contract.Requires(sink != null && predef != null);

     

-      if (f.Type is BoolType || f.Type is IntType || f.Type.IsTypeParameter) {

-        return;

-      }

-      

       Bpl.BoundVariable hVar = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$h", predef.HeapType));

       Bpl.Expr h = new Bpl.IdentifierExpr(f.tok, hVar);

       ExpressionTranslator etran = new ExpressionTranslator(this, predef, h);

@@ -652,69 +713,22 @@ namespace Microsoft.Dafny {
       Bpl.Expr o = new Bpl.IdentifierExpr(f.tok, oVar);

       

       // h[o,f]

-      Bpl.Expr oDotF = ExpressionTranslator.ReadHeap(f.tok, h, o, new Bpl.IdentifierExpr(f.tok, GetField(f)));

-      // $IsGoodHeap(h) && o != null && h[o,alloc]

-      Bpl.Expr ante = Bpl.Expr.And(Bpl.Expr.And(

-        FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, h),

-        Bpl.Expr.Neq(o, predef.Null)),

-        etran.IsAlloced(f.tok, o));

-

-      if (f.Type is SetType) {

-        SetType st = (SetType)f.Type;

-        if (st.Arg.IsRefType) {

-          //   axiom (forall h: [ref, Field x]x, o: ref, t: BoxType ::

-          //        { h[o,f][t] }

-          //        $IsGoodHeap(h) && o != null && h[o,alloc] && h[o,f][t] ==> UnBox(t) == null || h[UnBox(t), alloc]);

-          Bpl.BoundVariable tVar = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$t", predef.BoxType));

-          Bpl.Expr t = new Bpl.IdentifierExpr(f.tok, tVar);

-          Bpl.Expr oDotFsubT = Bpl.Expr.SelectTok(f.tok, oDotF, t);

-          Bpl.Expr unboxT = FunctionCall(f.tok, BuiltinFunction.Unbox, predef.RefType, t);

-

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

-          

-          Bpl.Expr goodRef = etran.GoodRef(f.tok, unboxT, st.Arg);

-          Bpl.Expr body = Bpl.Expr.Imp(Bpl.Expr.And(ante, oDotFsubT), Bpl.Expr.Or(Bpl.Expr.Eq(unboxT, predef.Null), goodRef));

-          Bpl.Expr ax = new Bpl.ForallExpr(f.tok, new Bpl.VariableSeq(hVar, oVar, tVar), tr, body);

-          sink.TopLevelDeclarations.Add(new Bpl.Axiom(f.tok, ax));

-        } else {

-          // TODO: should also handle sets of sets, etc.  This will probably require some extra predicates, and these predicates may even replace the above treatment of sets.

-        }

-        

-      } else if (f.Type is SeqType) {

-        SeqType st = (SeqType)f.Type;

-        if (st.Arg.IsRefType) {

-          //   axiom (forall h: [ref, Field x]x, o: ref, i: int ::

-          //        { Seq#Index(h[o,f], i) }

-          //        $IsGoodHeap(h) && o != null && h[o,alloc] && 0 <= i && i < Seq#Length(h[o,f]) ==> Unbox(Seq#Index(h[o,f], i)) == null || h[Unbox(Seq#Index(h[o,f], i)), alloc]);

-          Bpl.BoundVariable iVar = new Bpl.BoundVariable(f.tok, new Bpl.TypedIdent(f.tok, "$i", Bpl.Type.Int));

-          Bpl.Expr i = new Bpl.IdentifierExpr(f.tok, iVar);

-          Bpl.Expr oDotFsubI = FunctionCall(f.tok, BuiltinFunction.SeqIndex, predef.BoxType, oDotF, i);

-          Bpl.Expr unbox = FunctionCall(f.tok, BuiltinFunction.Unbox, predef.RefType, oDotFsubI);

-          

-          Bpl.Expr range = InSeqRange(f.tok, i, oDotF, true, null, false);

-          

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

-          

-          Bpl.Expr goodRef = etran.GoodRef(f.tok, unbox, st.Arg);

-          Bpl.Expr body = Bpl.Expr.Imp(Bpl.Expr.And(ante, range), Bpl.Expr.Or(Bpl.Expr.Eq(unbox, predef.Null), goodRef));

-          Bpl.Expr ax = new Bpl.ForallExpr(f.tok, new Bpl.VariableSeq(hVar, oVar, iVar), tr, body);

-          sink.TopLevelDeclarations.Add(new Bpl.Axiom(f.tok, ax));

-        } else {

-          // TODO: should also handle sequences of sequences, etc.  This will probably require some extra predicates, and these predicates may even replace the above treatment of sequences.

-        }

-      

-      } else if (f.Type.IsDatatype) {

-        // TODO

-        

+      Bpl.Expr oDotF;

+      if (f.IsMutable) {

+        oDotF = ExpressionTranslator.ReadHeap(f.tok, h, o, new Bpl.IdentifierExpr(f.tok, GetField(f)));

       } else {

-        // reference type:

-        //   axiom (forall h: [ref, Field x]x, o: ref ::

-        //        { h[o,f] }

-        //        $IsGoodHeap(h) && o != null && h[o,alloc] ==> h[o,f] == null || h[h[o,f], alloc]);

+        oDotF = new Bpl.NAryExpr(f.tok, new Bpl.FunctionCall(GetReadonlyField(f)), new Bpl.ExprSeq(o));

+      }

+

+      Bpl.Expr wh = GetWhereClause(f.tok, oDotF, f.Type, etran);

+      if (wh != null) {

+        // ante:  $IsGoodHeap(h) && o != null && h[o,alloc]

+        Bpl.Expr ante = Bpl.Expr.And(Bpl.Expr.And(

+          FunctionCall(f.tok, BuiltinFunction.IsGoodHeap, null, h),

+          Bpl.Expr.Neq(o, predef.Null)),

+          etran.IsAlloced(f.tok, o));

+        Bpl.Expr body = Bpl.Expr.Imp(ante, wh);

         Bpl.Trigger tr = new Bpl.Trigger(f.tok, true, new Bpl.ExprSeq(oDotF));

-        

-        Bpl.Expr goodRef = etran.GoodRef(f.tok, oDotF, f.Type);

-        Bpl.Expr body = Bpl.Expr.Imp(ante, Bpl.Expr.Or(Bpl.Expr.Eq(oDotF, predef.Null), goodRef));

         Bpl.Expr ax = new Bpl.ForallExpr(f.tok, new Bpl.VariableSeq(hVar, oVar), tr, body);

         sink.TopLevelDeclarations.Add(new Bpl.Axiom(f.tok, ax));

       }

@@ -816,20 +830,12 @@ 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 (forall<alpha> o: ref, f: Field alpha :: { $Heap[o,f] } $_Frame[o] || $Heap[o,f] == old($Heap)[o,f]);

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

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

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

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

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

-

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

-        Bpl.Expr oldHeapOF = ExpressionTranslator.ReadHeap(m.tok, etran.Old.HeapExpr, o, f);

-        Bpl.Expr inEnclosingFrame = Bpl.Expr.Select(etran.Old.TheFrame(m.tok), o, f);

-        Bpl.Expr body = Bpl.Expr.Or(inEnclosingFrame, Bpl.Expr.Eq(heapOF, oldHeapOF));

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

-        Bpl.Expr qq = new Bpl.ForallExpr(m.tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fVar), null, tr, body);

-        builder.Add(new Bpl.AssumeCmd(m.tok, qq));

+        // assume the usual two-state boilerplate information

+        foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(m.tok, currentMethod, etran.Old, etran)) {

+          if (tri.IsFree) {

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

+          }

+        }

 

         // also play havoc with the out parameters

         if (outParams.Length != 0) {  // don't create an empty havoc statement

@@ -917,8 +923,8 @@ namespace Microsoft.Dafny {
 

     void CheckFrameSubset(IToken tok, List<FrameExpression/*!*/>/*!*/ calleeFrame,

                           Expression receiverReplacement, Dictionary<IVariable,Expression/*!*/> substMap,

-                          ExpressionTranslator/*!*/ etran, Bpl.StmtListBuilder/*!*/ builder, string errorMessage)

-     

+                          ExpressionTranslator/*!*/ etran, Bpl.StmtListBuilder/*!*/ builder, string errorMessage,

+                          Bpl.QKeyValue kv)

     {

       Contract.Requires(tok != null);

       Contract.Requires(cce.NonNullElements(calleeFrame));

@@ -928,6 +934,7 @@ namespace Microsoft.Dafny {
       Contract.Requires(builder != null);

       Contract.Requires(errorMessage != null);

       Contract.Requires(predef != null);

+

       // emit: assert (forall<alpha> o: ref, f: Field alpha :: o != null && $Heap[o,alloc] && (o,f) in calleeFrame ==> $_Frame[o,f]);

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

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

@@ -939,7 +946,7 @@ namespace Microsoft.Dafny {
       Bpl.Expr inEnclosingFrame = Bpl.Expr.Select(etran.TheFrame(tok), o, f);

       Bpl.Expr q = new Bpl.ForallExpr(tok, new Bpl.TypeVariableSeq(alpha), new Bpl.VariableSeq(oVar, fVar),

                                       Bpl.Expr.Imp(Bpl.Expr.And(ante, oInCallee), inEnclosingFrame));

-      builder.Add(Assert(tok, q, errorMessage));

+      builder.Add(Assert(tok, q, errorMessage, kv));

     }

     

     /// <summary>

@@ -1046,19 +1053,19 @@ namespace Microsoft.Dafny {
     }

     

     Bpl.Expr/*!*/ InRWClause(IToken/*!*/ tok, Bpl.Expr/*!*/ o, Bpl.Expr/*!*/ f, List<FrameExpression/*!*/>/*!*/ rw, ExpressionTranslator/*!*/ etran,

-                         Expression receiverReplacement, Dictionary<IVariable,Expression/*!*/> substMap){

+                             Expression receiverReplacement, Dictionary<IVariable,Expression/*!*/> substMap) {

       Contract.Requires(tok != null);

       Contract.Requires(o != null);

       Contract.Requires(f != null);

       Contract.Requires(etran != null);

       Contract.Requires(cce.NonNullElements(rw));

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

-     Contract.Requires(predef != null);Contract.Requires(receiverReplacement == null && substMap == null);

+      Contract.Requires(predef != null);

+      Contract.Requires((receiverReplacement == null) == (substMap == null));

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

 

       // requires o to denote an expression of type RefType

       // "rw" is is allowed to contain a WildcardExpr

-     

     

       Bpl.Expr disjunction = null;

       foreach (FrameExpression rwComponent in rw) {

@@ -1194,10 +1201,11 @@ namespace Microsoft.Dafny {
       sink.TopLevelDeclarations.Add(impl);

     }

 

-    Bpl.Expr CtorInvocation(MatchCaseExpr mc, ExpressionTranslator etran, Bpl.VariableSeq locals) {

+    Bpl.Expr CtorInvocation(MatchCase mc, ExpressionTranslator etran, Bpl.VariableSeq locals, StmtListBuilder localTypeAssumptions) {

       Contract.Requires(mc != null);

       Contract.Requires(etran != null);

       Contract.Requires(locals != null);

+      Contract.Requires(localTypeAssumptions != null);

       Contract.Requires(predef != null);

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

 

@@ -1206,10 +1214,11 @@ namespace Microsoft.Dafny {
         BoundVar p = mc.Arguments[i];

         Bpl.Variable local = new Bpl.LocalVariable(p.tok, new Bpl.TypedIdent(p.tok, p.UniqueName, TrType(p.Type)));

         locals.Add(local);

-        IdentifierExpr ie = new IdentifierExpr(p.tok, p.UniqueName);

-        ie.Var = p; ie.Type = ie.Var.Type;  // resolve it here

-

         Type t = mc.Ctor.Formals[i].Type;

+        Bpl.Expr wh = GetWhereClause(p.tok, new Bpl.IdentifierExpr(p.tok, local), p.Type, etran);

+        if (wh != null) {

+          localTypeAssumptions.Add(new Bpl.AssumeCmd(p.tok, wh));

+        }

         args.Add(etran.CondApplyBox(mc.tok, new Bpl.IdentifierExpr(p.tok, local), cce.NonNull(p.Type), t));

       }

       Bpl.IdentifierExpr id = new Bpl.IdentifierExpr(mc.tok, mc.Ctor.FullName, predef.DatatypeType);

@@ -1304,6 +1313,9 @@ namespace Microsoft.Dafny {
       } else if (expr is FreshExpr) {

         FreshExpr e = (FreshExpr)expr;

         return IsTotal(e.E, etran);

+      } else if (expr is AllocatedExpr) {

+        AllocatedExpr e = (AllocatedExpr)expr;

+        return IsTotal(e.E, etran);

       } else if (expr is UnaryExpr) {

         UnaryExpr e = (UnaryExpr)expr;

         Bpl.Expr t = IsTotal(e.E, etran);

@@ -1338,10 +1350,8 @@ namespace Microsoft.Dafny {
         Bpl.Expr total = IsTotal(e.Body, etran);

         if (total != Bpl.Expr.True) {

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

-          foreach (BoundVar bv in e.BoundVars) {

-            bvars.Add(new Bpl.BoundVariable(bv.tok, new Bpl.TypedIdent(bv.tok, bv.UniqueName, TrType(bv.Type))));

-          }

-          total = new Bpl.ForallExpr(expr.tok, bvars, total);

+          Bpl.Expr typeAntecedent = etran.TrBoundVariables(e, bvars);

+          total = new Bpl.ForallExpr(expr.tok, bvars, Bpl.Expr.Imp(typeAntecedent, total));

         }

         return total;

       } else if (expr is ITEExpr) {

@@ -1368,7 +1378,134 @@ namespace Microsoft.Dafny {
       }

       return total;

     }

-    

+

+    Bpl.Expr CanCallAssumption(Expression expr, ExpressionTranslator etran) {

+      Contract.Requires(expr != null);

+      Contract.Requires(etran != null);

+      Contract.Requires(predef != null);

+      Contract.Ensures(Contract.Result<Bpl.Expr>() != null);

+

+      if (expr is LiteralExpr || expr is ThisExpr || expr is IdentifierExpr || expr is WildcardExpr) {

+        return Bpl.Expr.True;

+      } else if (expr is DisplayExpression) {

+        DisplayExpression e = (DisplayExpression)expr;

+        return CanCallAssumption(e.Elements, etran);

+      } else if (expr is FieldSelectExpr) {

+        FieldSelectExpr e = (FieldSelectExpr)expr;

+        if (e.Obj is ThisExpr) {

+          return Bpl.Expr.True;

+        } else {

+          Bpl.Expr r = CanCallAssumption(e.Obj, etran);

+          return r;

+        }

+      } else if (expr is SeqSelectExpr) {

+        SeqSelectExpr e = (SeqSelectExpr)expr;

+        bool isSequence = e.Seq.Type is SeqType;

+        Bpl.Expr total = CanCallAssumption(e.Seq, etran);

+        Bpl.Expr seq = etran.TrExpr(e.Seq);

+        Bpl.Expr e0 = null;

+        if (e.E0 != null) {

+          e0 = etran.TrExpr(e.E0);

+          total = BplAnd(total, CanCallAssumption(e.E0, etran));

+        }

+        if (e.E1 != null) {

+          total = BplAnd(total, CanCallAssumption(e.E1, etran));

+        }

+        return total;

+      } else if (expr is MultiSelectExpr) {

+        MultiSelectExpr e = (MultiSelectExpr)expr;

+        Bpl.Expr total = CanCallAssumption(e.Array, etran);

+        foreach (Expression idx in e.Indices) {

+          total = BplAnd(total, CanCallAssumption(idx, etran));

+        }

+        return total;

+      } else if (expr is SeqUpdateExpr) {

+        SeqUpdateExpr e = (SeqUpdateExpr)expr;

+        Bpl.Expr total = CanCallAssumption(e.Seq, etran);

+        Bpl.Expr seq = etran.TrExpr(e.Seq);

+        Bpl.Expr index = etran.TrExpr(e.Index);

+        total = BplAnd(total, CanCallAssumption(e.Index, etran));

+        total = BplAnd(total, CanCallAssumption(e.Value, etran));

+        return total;

+      } else if (expr is FunctionCallExpr) {

+        FunctionCallExpr e = (FunctionCallExpr)expr;

+        Contract.Assert(e.Function != null);  // follows from the fact that expr has been successfully resolved

+        // check well-formedness of receiver

+        Bpl.Expr r = CanCallAssumption(e.Receiver, etran);

+        // check well-formedness of the other parameters

+        r = BplAnd(r, CanCallAssumption(e.Args, etran));

+        // get to assume canCall

+        Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(expr.tok, e.Function.FullName + "#canCall", Bpl.Type.Bool);

+        ExprSeq args = etran.FunctionInvocationArguments(e);

+        Bpl.Expr canCallFuncAppl = new Bpl.NAryExpr(expr.tok, new Bpl.FunctionCall(canCallFuncID), args);

+        r = BplAnd(r, canCallFuncAppl);

+        return r;

+      } else if (expr is DatatypeValue) {

+        DatatypeValue dtv = (DatatypeValue)expr;

+        return CanCallAssumption(dtv.Arguments, etran);

+      } else if (expr is OldExpr) {

+        OldExpr e = (OldExpr)expr;

+        return new Bpl.OldExpr(expr.tok, CanCallAssumption(e.E, etran));

+      } else if (expr is FreshExpr) {

+        FreshExpr e = (FreshExpr)expr;

+        return CanCallAssumption(e.E, etran);

+      } else if (expr is AllocatedExpr) {

+        AllocatedExpr e = (AllocatedExpr)expr;

+        return CanCallAssumption(e.E, etran);

+      } else if (expr is UnaryExpr) {

+        UnaryExpr e = (UnaryExpr)expr;

+        Bpl.Expr t = CanCallAssumption(e.E, etran);

+        return t;

+      } else if (expr is BinaryExpr) {

+        BinaryExpr e = (BinaryExpr)expr;

+        Bpl.Expr t0 = CanCallAssumption(e.E0, etran);

+        Bpl.Expr t1 = CanCallAssumption(e.E1, etran);

+        switch (e.ResolvedOp) {

+          case BinaryExpr.ResolvedOpcode.And:

+          case BinaryExpr.ResolvedOpcode.Imp:

+            t1 = Bpl.Expr.Imp(etran.TrExpr(e.E0), t1);

+            break;

+          case BinaryExpr.ResolvedOpcode.Or:

+            t1 = Bpl.Expr.Imp(Bpl.Expr.Not(etran.TrExpr(e.E0)), t1);

+            break;

+          default:

+            break;

+        }

+        return BplAnd(t0, t1);

+      } else if (expr is QuantifierExpr) {

+        QuantifierExpr e = (QuantifierExpr)expr;

+        Bpl.Expr total = CanCallAssumption(e.Body, etran);

+        if (total != Bpl.Expr.True) {

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

+          Bpl.Expr typeAntecedent = etran.TrBoundVariables(e, bvars);

+          total = new Bpl.ForallExpr(expr.tok, bvars, Bpl.Expr.Imp(typeAntecedent, total));

+        }

+        return total;

+      } else if (expr is ITEExpr) {

+        ITEExpr e = (ITEExpr)expr;

+        Bpl.Expr total = CanCallAssumption(e.Test, etran);

+        Bpl.Expr test = etran.TrExpr(e.Test);

+        total = BplAnd(total, Bpl.Expr.Imp(test, CanCallAssumption(e.Thn, etran)));

+        total = BplAnd(total, Bpl.Expr.Imp(Bpl.Expr.Not(test), CanCallAssumption(e.Els, etran)));

+        return total;

+      } else {

+        Contract.Assert(false); throw new cce.UnreachableException();  // unexpected expression

+      }

+    }

+

+    Bpl.Expr/*!*/ CanCallAssumption(List<Expression/*!*/>/*!*/ exprs, ExpressionTranslator/*!*/ etran) {

+      Contract.Requires(etran != null);

+      Contract.Requires(exprs != null);

+      Contract.Ensures(Contract.Result<Bpl.Expr>() != null);

+

+      Bpl.Expr total = Bpl.Expr.True;

+      foreach (Expression e in exprs) {

+        Contract.Assert(e != null);

+        total = BplAnd(total, CanCallAssumption(e, etran));

+      }

+      return total;

+    }

+

     Bpl.Expr BplAnd(Bpl.Expr a, Bpl.Expr b) {

       Contract.Requires(a != null);

       Contract.Requires(b != null);

@@ -1383,7 +1520,7 @@ namespace Microsoft.Dafny {
       }

     }

     

-    void CheckNonNull(IToken tok, Expression e, Bpl.StmtListBuilder builder, ExpressionTranslator etran){

+    void CheckNonNull(IToken tok, Expression e, Bpl.StmtListBuilder builder, ExpressionTranslator etran, Bpl.QKeyValue kv) {

       Contract.Requires(tok != null);

       Contract.Requires(e != null);

       Contract.Requires(builder != null);

@@ -1393,7 +1530,7 @@ namespace Microsoft.Dafny {
       if (e is ThisExpr) {

         // already known to be non-null

       } else {

-        builder.Add(Assert(tok, Bpl.Expr.Neq(etran.TrExpr(e), predef.Null), "target object may be null"));

+        builder.Add(Assert(tok, Bpl.Expr.Neq(etran.TrExpr(e), predef.Null), "target object may be null", kv));

       }

     }

 

@@ -1413,12 +1550,35 @@ namespace Microsoft.Dafny {
       public readonly Function Decr;

       public readonly Function SelfCallsAllowance;

       public readonly bool DoReadsChecks;

+      public readonly Bpl.QKeyValue AssertKv;

       public WFOptions() { }

       public WFOptions(Function decr, Function selfCallsAllowance, bool doReadsChecks) {

         Decr = decr;

         SelfCallsAllowance = selfCallsAllowance;

         DoReadsChecks = doReadsChecks;

       }

+      public WFOptions(Bpl.QKeyValue kv) {

+        AssertKv = kv;

+      }

+    }

+

+    void TrStmt_CheckWellformed(Expression expr, Bpl.StmtListBuilder builder, Bpl.VariableSeq locals, ExpressionTranslator etran, bool subsumption) {

+      Contract.Requires(expr != null);

+      Contract.Requires(builder != null);

+      Contract.Requires(locals != null);

+      Contract.Requires(etran != null);

+

+      Bpl.QKeyValue kv;

+      if (subsumption) {

+        kv = null;  // this is the default behavior of Boogie's assert

+      } else {

+        List<object> args = new List<object>();

+        // {:subsumption 0}

+        args.Add(Bpl.Expr.Literal(0));

+        kv = new Bpl.QKeyValue(expr.tok, "subsumption", args, null);

+      }

+      CheckWellformed(expr, new WFOptions(kv), null, locals, builder, etran);

+      builder.Add(new Bpl.AssumeCmd(expr.tok, CanCallAssumption(expr, etran)));

     }

 

     /// <summary>

@@ -1428,7 +1588,7 @@ namespace Microsoft.Dafny {
     /// assume the equivalent of "result == expr".

     /// See class WFOptions for descriptions of the specified options.

     /// </summary>

-    void CheckWellformed(Expression expr, WFOptions options, Bpl.Expr result, Bpl.VariableSeq locals, Bpl.StmtListBuilder builder, ExpressionTranslator etran){

+    void CheckWellformed(Expression expr, WFOptions options, Bpl.Expr result, Bpl.VariableSeq locals, Bpl.StmtListBuilder builder, ExpressionTranslator etran) {

       Contract.Requires(expr != null);

       Contract.Requires(options != null);

       Contract.Requires(locals != null);

@@ -1446,9 +1606,9 @@ namespace Microsoft.Dafny {
       } else if (expr is FieldSelectExpr) {

         FieldSelectExpr e = (FieldSelectExpr)expr;

         CheckWellformed(e.Obj, options, null, locals, builder, etran);

-        CheckNonNull(expr.tok, e.Obj, builder, etran);

+        CheckNonNull(expr.tok, e.Obj, builder, etran, options.AssertKv);

         if (options.DoReadsChecks && e.Field.IsMutable) {

-          builder.Add(Assert(expr.tok, Bpl.Expr.SelectTok(expr.tok, etran.TheFrame(expr.tok), etran.TrExpr(e.Obj), GetField(e)), "insufficient reads clause to read field"));

+          builder.Add(Assert(expr.tok, Bpl.Expr.SelectTok(expr.tok, etran.TheFrame(expr.tok), etran.TrExpr(e.Obj), GetField(e)), "insufficient reads clause to read field", options.AssertKv));

         }

       } else if (expr is SeqSelectExpr) {

         SeqSelectExpr e = (SeqSelectExpr)expr;

@@ -1459,16 +1619,16 @@ namespace Microsoft.Dafny {
         if (e.E0 != null) {

           e0 = etran.TrExpr(e.E0);

           CheckWellformed(e.E0, options, null, locals, builder, etran);

-          builder.Add(Assert(expr.tok, InSeqRange(expr.tok, e0, seq, isSequence, null, !e.SelectOne), "index out of range"));

+          builder.Add(Assert(expr.tok, InSeqRange(expr.tok, e0, seq, isSequence, null, !e.SelectOne), "index out of range", options.AssertKv));

         }

         if (e.E1 != null) {

           CheckWellformed(e.E1, options, null, locals, builder, etran);

-          builder.Add(Assert(expr.tok, InSeqRange(expr.tok, etran.TrExpr(e.E1), seq, isSequence, e0, true), "end-of-range beyond length of " + (isSequence ? "sequence" : "array")));

+          builder.Add(Assert(expr.tok, InSeqRange(expr.tok, etran.TrExpr(e.E1), seq, isSequence, e0, true), "end-of-range beyond length of " + (isSequence ? "sequence" : "array"), options.AssertKv));

         }

         if (options.DoReadsChecks && cce.NonNull(e.Seq.Type).IsArrayType) {

           Contract.Assert(e.E0 != null);

           Bpl.Expr fieldName = FunctionCall(expr.tok, BuiltinFunction.IndexField, null, etran.TrExpr(e.E0));

-          builder.Add(Assert(expr.tok, Bpl.Expr.SelectTok(expr.tok, etran.TheFrame(expr.tok), seq, fieldName), "insufficient reads clause to read array element"));

+          builder.Add(Assert(expr.tok, Bpl.Expr.SelectTok(expr.tok, etran.TheFrame(expr.tok), seq, fieldName), "insufficient reads clause to read array element", options.AssertKv));

         }

       } else if (expr is MultiSelectExpr) {

         MultiSelectExpr e = (MultiSelectExpr)expr;

@@ -1482,7 +1642,7 @@ namespace Microsoft.Dafny {
           Bpl.Expr lower = Bpl.Expr.Le(Bpl.Expr.Literal(0), index);

           Bpl.Expr length = ArrayLength(idx.tok, array, e.Indices.Count, i);

           Bpl.Expr upper = Bpl.Expr.Lt(index, length);

-          builder.Add(Assert(idx.tok, Bpl.Expr.And(lower, upper), "index " + i + " out of range"));

+          builder.Add(Assert(idx.tok, Bpl.Expr.And(lower, upper), "index " + i + " out of range", options.AssertKv));

           i++;

         }

       } else if (expr is SeqUpdateExpr) {

@@ -1491,7 +1651,7 @@ namespace Microsoft.Dafny {
         Bpl.Expr seq = etran.TrExpr(e.Seq);

         Bpl.Expr index = etran.TrExpr(e.Index);

         CheckWellformed(e.Index, options, null, locals, builder, etran);

-        builder.Add(Assert(expr.tok, InSeqRange(expr.tok, index, seq, true, null, false), "index out of range"));

+        builder.Add(Assert(expr.tok, InSeqRange(expr.tok, index, seq, true, null, false), "index out of range", options.AssertKv));

         CheckWellformed(e.Value, options, null, locals, builder, etran);

       } else if (expr is FunctionCallExpr) {

         FunctionCallExpr e = (FunctionCallExpr)expr;

@@ -1499,7 +1659,7 @@ namespace Microsoft.Dafny {
         // check well-formedness of receiver

         CheckWellformed(e.Receiver, options, null, locals, builder, etran);

         if (!e.Function.IsStatic && !(e.Receiver is ThisExpr)) {

-          CheckNonNull(expr.tok, e.Receiver, builder, etran);

+          CheckNonNull(expr.tok, e.Receiver, builder, etran, options.AssertKv);

         }

         // check well-formedness of the other parameters

         foreach (Expression arg in e.Args) {

@@ -1520,18 +1680,37 @@ namespace Microsoft.Dafny {
           Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(p.tok, lhs, etran.CondApplyBox(p.tok, etran.TrExpr(ee), cce.NonNull(ee.Type), p.Type));

           builder.Add(cmd);

         }

+        // Check that every parameter is available in the state in which the function is invoked; this means checking that it has

+        // the right type and is allocated.  These checks usually hold trivially, on account of that the Dafny language only gives

+        // access to expressions of the appropriate type and that are allocated in the current state.  However, if the function is

+        // invoked in the 'old' state, then we need to check that its arguments were all available at that time as well.

+        if (etran.UsesOldHeap) {

+          if (!e.Function.IsStatic) {

+            Bpl.Expr wh = GetWhereClause(e.Receiver.tok, etran.TrExpr(e.Receiver), e.Receiver.Type, etran);

+            if (wh != null) {

+              builder.Add(Assert(e.Receiver.tok, wh, "receiver argument must be allocated in the state in which the function is invoked"));

+            }

+          }

+          for (int i = 0; i < e.Args.Count; i++) {

+            Expression ee = e.Args[i];

+            Bpl.Expr wh = GetWhereClause(ee.tok, etran.TrExpr(ee), ee.Type, etran);

+            if (wh != null) {

+              builder.Add(Assert(ee.tok, wh, "argument must be allocated in the state in which the function is invoked"));

+            }

+          }

+        }

         // check that the preconditions for the call hold

         foreach (Expression p in e.Function.Req) {

           Expression precond = Substitute(p, e.Receiver, substMap);

-          builder.Add(Assert(expr.tok, etran.TrExpr(precond), "possible violation of function precondition"));

+          builder.Add(Assert(expr.tok, etran.TrExpr(precond), "possible violation of function precondition", options.AssertKv));

         }

+        Bpl.Expr allowance = null;

         if (options.Decr != null || options.DoReadsChecks) {

           if (options.DoReadsChecks) {

             // check that the callee reads only what the caller is already allowed to read

-            CheckFrameSubset(expr.tok, e.Function.Reads, e.Receiver, substMap, etran, builder, "insufficient reads clause to invoke function");

+            CheckFrameSubset(expr.tok, e.Function.Reads, e.Receiver, substMap, etran, builder, "insufficient reads clause to invoke function", options.AssertKv);

           }

 

-          Bpl.Expr allowance = null;

           if (options.Decr != null) {

             // check that the decreases measure goes down

             ModuleDecl module = cce.NonNull(e.Function.EnclosingClass).Module;

@@ -1555,13 +1734,13 @@ namespace Microsoft.Dafny {
               }

             }

           }

-

-          // all is okay, so allow this function application access to the function's axiom, except if it was okay because of the self-call allowance.

-          Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(expr.tok, e.Function.FullName + "#canCall", Bpl.Type.Bool);

-          ExprSeq args = etran.FunctionInvocationArguments(e);

-          Bpl.Expr canCallFuncAppl = new Bpl.NAryExpr(expr.tok, new Bpl.FunctionCall(canCallFuncID), args);

-          builder.Add(new Bpl.AssumeCmd(expr.tok, allowance == null ? canCallFuncAppl : Bpl.Expr.Or(allowance, canCallFuncAppl)));

         }

+        // all is okay, so allow this function application access to the function's axiom, except if it was okay because of the self-call allowance.

+        Bpl.IdentifierExpr canCallFuncID = new Bpl.IdentifierExpr(expr.tok, e.Function.FullName + "#canCall", Bpl.Type.Bool);

+        ExprSeq args = etran.FunctionInvocationArguments(e);

+        Bpl.Expr canCallFuncAppl = new Bpl.NAryExpr(expr.tok, new Bpl.FunctionCall(canCallFuncID), args);

+        builder.Add(new Bpl.AssumeCmd(expr.tok, allowance == null ? canCallFuncAppl : Bpl.Expr.Or(allowance, canCallFuncAppl)));

+

       } else if (expr is DatatypeValue) {

         DatatypeValue dtv = (DatatypeValue)expr;

         foreach (Expression arg in dtv.Arguments) {

@@ -1573,11 +1752,14 @@ namespace Microsoft.Dafny {
       } else if (expr is FreshExpr) {

         FreshExpr e = (FreshExpr)expr;

         CheckWellformed(e.E, options, null, locals, builder, etran);

+      } else if (expr is AllocatedExpr) {

+        AllocatedExpr e = (AllocatedExpr)expr;

+        CheckWellformed(e.E, options, null, locals, builder, etran);

       } else if (expr is UnaryExpr) {

         UnaryExpr e = (UnaryExpr)expr;

         CheckWellformed(e.E, options, null, locals, builder, etran);

         if (e.Op == UnaryExpr.Opcode.SeqLength && !(e.E.Type is SeqType)) {

-          CheckNonNull(expr.tok, e.E, builder, etran);

+          CheckNonNull(expr.tok, e.E, builder, etran, options.AssertKv);

         }

       } else if (expr is BinaryExpr) {

         BinaryExpr e = (BinaryExpr)expr;

@@ -1601,7 +1783,7 @@ namespace Microsoft.Dafny {
           case BinaryExpr.ResolvedOpcode.Div:

           case BinaryExpr.ResolvedOpcode.Mod:

             CheckWellformed(e.E1, options, null, locals, builder, etran);

-            builder.Add(Assert(expr.tok, Bpl.Expr.Neq(etran.TrExpr(e.E1), Bpl.Expr.Literal(0)), "possible division by zero"));

+            builder.Add(Assert(expr.tok, Bpl.Expr.Neq(etran.TrExpr(e.E1), Bpl.Expr.Literal(0)), "possible division by zero", options.AssertKv));

             break;

           default:

             CheckWellformed(e.E1, options, null, locals, builder, etran);

@@ -1617,7 +1799,12 @@ namespace Microsoft.Dafny {
           IdentifierExpr ie = new IdentifierExpr(local.Tok, local.UniqueName);

           ie.Var = local;  ie.Type = ie.Var.Type;  // resolve ie here

           substMap.Add(bv, ie);

-          locals.Add(new Bpl.LocalVariable(local.Tok, new Bpl.TypedIdent(local.Tok, local.UniqueName, TrType(local.Type))));

+          Bpl.LocalVariable bvar = new Bpl.LocalVariable(local.Tok, new Bpl.TypedIdent(local.Tok, local.UniqueName, TrType(local.Type)));

+          locals.Add(bvar);

+          Bpl.Expr wh = GetWhereClause(bv.tok, new Bpl.IdentifierExpr(bvar.tok, bvar), local.Type, etran);

+          if (wh != null) {

+            builder.Add(new Bpl.AssumeCmd(bv.tok, wh));

+          }

         }

         Expression body = Substitute(e.Body, null, substMap);

         CheckWellformed(body, options, null, locals, builder, etran);

@@ -1641,12 +1828,13 @@ namespace Microsoft.Dafny {
         StmtList els = elsBldr.Collect(expr.tok);

         for (int i = me.Cases.Count; 0 <= --i; ) {

           MatchCaseExpr mc = me.Cases[i];

-          Bpl.Expr ct = CtorInvocation(mc, etran, locals);

-          // generate:  if (src == ctor(args)) { mc.Body is well-formed; assume Result == TrExpr(case); } else ...

           Bpl.StmtListBuilder b = new Bpl.StmtListBuilder();

+          Bpl.Expr ct = CtorInvocation(mc, etran, locals, b);

+          // generate:  if (src == ctor(args)) { assume args-is-well-typed; mc.Body is well-formed; assume Result == TrExpr(case); } else ...

           CheckWellformed(mc.Body, options, null, locals, b, etran);

           if (result != null) {

             b.Add(new Bpl.AssumeCmd(mc.tok, Bpl.Expr.Eq(result, etran.TrExpr(mc.Body))));

+            b.Add(new Bpl.AssumeCmd(mc.tok, CanCallAssumption(mc.Body, etran)));

           }

           ifcmd = new Bpl.IfCmd(mc.tok, Bpl.Expr.Eq(src, ct), b.Collect(mc.tok), ifcmd, els);

           els = null;

@@ -1660,6 +1848,7 @@ namespace Microsoft.Dafny {
 

       if (result != null) {

         builder.Add(new Bpl.AssumeCmd(expr.tok, Bpl.Expr.Eq(result, etran.TrExpr(expr))));

+        builder.Add(new Bpl.AssumeCmd(expr.tok, CanCallAssumption(expr, etran)));

       }

     }

 

@@ -1701,6 +1890,68 @@ namespace Microsoft.Dafny {
       return decr;

     }

 

+    List<Expression> LoopDecreasesWithDefault(WhileStmt s, out bool inferredDecreases) {

+      Contract.Requires(s != null);

+

+      List<Expression> theDecreases = s.Decreases;

+      inferredDecreases = false;

+      if (theDecreases.Count == 0 && s.Guard != null) {

+        theDecreases = new List<Expression>();

+        Expression prefix = null;

+        foreach (Expression guardConjunct in Conjuncts(s.Guard)) {

+          Expression guess = null;

+          BinaryExpr bin = guardConjunct as BinaryExpr;

+          if (bin != null) {

+            switch (bin.ResolvedOp) {

+              case BinaryExpr.ResolvedOpcode.Lt:

+              case BinaryExpr.ResolvedOpcode.Le:

+                // for A < B and A <= B, use the decreases B - A

+                guess = CreateIntSub(s.Tok, bin.E1, bin.E0);

+                break;

+              case BinaryExpr.ResolvedOpcode.Ge:

+              case BinaryExpr.ResolvedOpcode.Gt:

+                // for A >= B and A > B, use the decreases A - B

+                guess = CreateIntSub(s.Tok, bin.E0, bin.E1);

+                break;

+              case BinaryExpr.ResolvedOpcode.NeqCommon:

+                if (bin.E0.Type is IntType) {

+                  // for A != B where A and B are integers, use the absolute difference between A and B (that is: if 0 <= A-B then A-B else B-A)

+                  Expression AminusB = CreateIntSub(s.Tok, bin.E0, bin.E1);

+                  Expression BminusA = CreateIntSub(s.Tok, bin.E1, bin.E0);

+                  Expression zero = CreateIntLiteral(s.Tok, 0);

+                  BinaryExpr test = new BinaryExpr(s.Tok, BinaryExpr.Opcode.Le, zero, AminusB);

+                  test.ResolvedOp = BinaryExpr.ResolvedOpcode.Le;  // resolve here

+                  test.Type = Type.Bool;  // resolve here

+                  guess = CreateIntITE(s.Tok, test, AminusB, BminusA);

+                }

+                break;

+              default:

+                break;

+            }

+          }

+          if (guess != null) {

+            if (prefix != null) {

+              // Make the following guess:  if prefix then guess else -1

+              Expression negativeOne = CreateIntLiteral(s.Tok, -1);

+              guess = CreateIntITE(s.Tok, prefix, guess, negativeOne);

+            }

+            theDecreases.Add(guess);

+            inferredDecreases = true;

+            break;  // ignore any further conjuncts

+          }

+          if (prefix == null) {

+            prefix = guardConjunct;

+          } else {

+            BinaryExpr and = new BinaryExpr(s.Tok, BinaryExpr.Opcode.And, prefix, guardConjunct);

+            and.ResolvedOp = BinaryExpr.ResolvedOpcode.And;  // resolve here

+            and.Type = Type.Bool;  // resolve here

+            prefix = and;

+          }

+        }

+      }

+      return theDecreases;

+    }

+

     Expression FrameToObjectSet(List<FrameExpression> fexprs) {

       Contract.Requires(fexprs != null);

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

@@ -1749,9 +2000,9 @@ namespace Microsoft.Dafny {
     }

     

     Bpl.Constant GetClass(TopLevelDecl cl)

-     {

+    {

       Contract.Requires(cl != null);

- Contract.Requires(predef != null);

+      Contract.Requires(predef != null);

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

 

       Bpl.Constant cc;

@@ -1765,7 +2016,7 @@ namespace Microsoft.Dafny {
     }

     

     Bpl.Expr GetTypeExpr(IToken tok, Type type)

-     {

+    {

       Contract.Requires(tok != null);

       Contract.Requires(type != null);

       Contract.Requires(predef != null);

@@ -2369,6 +2620,17 @@ namespace Microsoft.Dafny {
       return cmd;

     }

 

+    Bpl.AssertCmd Assert(Bpl.IToken tok, Bpl.Expr condition, string errorMessage, Bpl.QKeyValue kv) {

+      Contract.Requires(tok != null);

+      Contract.Requires(errorMessage != null);

+      Contract.Requires(condition != null);

+      Contract.Ensures(Contract.Result<Bpl.AssertCmd>() != null);

+

+      Bpl.AssertCmd cmd = new Bpl.AssertCmd(tok, condition, kv);

+      cmd.ErrorData = "Error: " + errorMessage;

+      return cmd;

+    }

+

     Bpl.Ensures Ensures(IToken tok, bool free, Bpl.Expr condition, string errorMessage, string comment)

     {

       Contract.Requires(tok != null);

@@ -2429,7 +2691,7 @@ namespace Microsoft.Dafny {
       if (stmt is AssertStmt) {

         AddComment(builder, stmt, "assert statement");

         AssertStmt s = (AssertStmt)stmt;

-        builder.Add(AssertNS(s.Expr.tok, IsTotal(s.Expr, etran), "assert condition must be well defined"));  // totality check

+        TrStmt_CheckWellformed(s.Expr, builder, locals, etran, false);

         List<Expression> definitions, pieces;

         if (!SplitExpr(s.Expr, out definitions, out pieces)) {

           builder.Add(Assert(s.Expr.tok, etran.TrExpr(s.Expr), "assertion violation"));

@@ -2445,20 +2707,20 @@ namespace Microsoft.Dafny {
       } else if (stmt is AssumeStmt) {

         AddComment(builder, stmt, "assume statement");

         AssumeStmt s = (AssumeStmt)stmt;

-        builder.Add(AssertNS(stmt.Tok, IsTotal(s.Expr, etran), "assume condition must be well defined"));  // totality check

+        TrStmt_CheckWellformed(s.Expr, builder, locals, etran, false);

         builder.Add(new Bpl.AssumeCmd(stmt.Tok, etran.TrExpr(s.Expr)));

       } else if (stmt is UseStmt) {

         AddComment(builder, stmt, "use statement");

         UseStmt s = (UseStmt)stmt;

-        // Skip the totality check.  This makes the 'use' statement easier to use and it has no executable analog anyhow

-        // builder.Add(Assert(stmt.Tok, IsTotal(s.Expr, etran), "use expression must be well defined"));  // totality check

+        // Skip the definedness check.  This makes the 'use' statement easier to use and it has no executable analog anyhow

+        // TrStmt_CheckWellformed(s.Expr, builder, locals, etran);

         builder.Add(new Bpl.AssumeCmd(stmt.Tok, (s.EvalInOld ? etran.Old : etran).TrUseExpr(s.FunctionCallExpr)));

       } else if (stmt is PrintStmt) {

         AddComment(builder, stmt, "print statement");

         PrintStmt s = (PrintStmt)stmt;

         foreach (Attributes.Argument arg in s.Args) {

           if (arg.E != null) {

-            builder.Add(AssertNS(stmt.Tok, IsTotal(arg.E, etran), "print expression must be well defined"));  // totality check

+            TrStmt_CheckWellformed(arg.E, builder, locals, etran, false);

           }

         }

         

@@ -2516,7 +2778,7 @@ namespace Microsoft.Dafny {
           

           Bpl.IdentifierExpr lhs = (Bpl.IdentifierExpr)etran.TrExpr(ie);  // TODO: is this cast always justified?

           Expression actual = s.Args[i];

-          builder.Add(Assert(actual.tok, IsTotal(actual, etran), "argument must be well defined"));  // totality check

+          TrStmt_CheckWellformed(actual, builder, locals, etran, true);

           Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(p.tok, lhs, etran.CondApplyBox(stmt.Tok, etran.TrExpr(actual), cce.NonNull(actual.Type), s.Method.Ins[i].Type));

           builder.Add(cmd);

           ins.Add(lhs);

@@ -2541,7 +2803,7 @@ namespace Microsoft.Dafny {
         }

 

         // Check modifies clause

-        CheckFrameSubset(stmt.Tok, s.Method.Mod, s.Receiver, substMap, etran, builder, "call may violate caller's modifies clause");

+        CheckFrameSubset(stmt.Tok, s.Method.Mod, s.Receiver, substMap, etran, builder, "call may violate caller's modifies clause", null);

 

         // Check termination

         ModuleDecl module = cce.NonNull(s.Method.EnclosingClass).Module;

@@ -2562,8 +2824,15 @@ namespace Microsoft.Dafny {
           IdentifierExpr e = s.Lhs[i];

           Bpl.IdentifierExpr lhs = (Bpl.IdentifierExpr)etran.TrExpr(e);  // TODO: is this cast always justified?

           if (tmpVarIdE != null) {

-            // e := UnBox(tmpVar);

-            Bpl.Cmd cmd = Bpl.Cmd.SimpleAssign(stmt.Tok, lhs, FunctionCall(stmt.Tok, BuiltinFunction.Unbox, TrType(cce.NonNull(e.Type)), tmpVarIdE));

+            // Instead of an assignment:

+            //    e := UnBox(tmpVar);

+            // we use:

+            //    havoc e; assume e == UnBox(tmpVar);

+            // because that will reap the benefits of e's where clause, so that some additional type information will be known about

+            // the out-parameter.

+            Bpl.Cmd cmd = new Bpl.HavocCmd(stmt.Tok, new IdentifierExprSeq(lhs));

+            builder.Add(cmd);

+            cmd = new Bpl.AssumeCmd(stmt.Tok, Bpl.Expr.Eq(lhs, FunctionCall(stmt.Tok, BuiltinFunction.Unbox, TrType(cce.NonNull(e.Type)), tmpVarIdE)));

             builder.Add(cmd);

           }

         }

@@ -2580,7 +2849,7 @@ namespace Microsoft.Dafny {
         if (s.Guard == null) {

           guard = null;

         } else {

-          builder.Add(Assert(s.Guard.tok, IsTotal(s.Guard, etran), "if guard must be well defined"));  // totality check

+          TrStmt_CheckWellformed(s.Guard, builder, locals, etran, true);

           guard = etran.TrExpr(s.Guard);

         }

         Bpl.StmtListBuilder b = new Bpl.StmtListBuilder();

@@ -2610,61 +2879,8 @@ namespace Microsoft.Dafny {
         loopHeapVarCount++;

         

         // use simple heuristics to create a default decreases clause, if none is given

-        List<Expression> theDecreases = s.Decreases;

-        bool inferredDecreases = false;

-        if (theDecreases.Count == 0 && s.Guard != null) {

-          Expression prefix = null;

-          foreach (Expression guardConjunct in Conjuncts(s.Guard)) {

-            Expression guess = null;

-            BinaryExpr bin = guardConjunct as BinaryExpr;

-            if (bin != null) {

-              switch (bin.ResolvedOp) {

-                case BinaryExpr.ResolvedOpcode.Lt:

-                case BinaryExpr.ResolvedOpcode.Le:

-                  // for A < B and A <= B, use the decreases B - A

-                  guess = CreateIntSub(s.Tok, bin.E1, bin.E0);

-                  break;

-                case BinaryExpr.ResolvedOpcode.Ge:

-                case BinaryExpr.ResolvedOpcode.Gt:

-                  // for A >= B and A > B, use the decreases A - B

-                  guess = CreateIntSub(s.Tok, bin.E0, bin.E1);

-                  break;

-                case BinaryExpr.ResolvedOpcode.NeqCommon:

-                  if (bin.E0.Type is IntType) {

-                    // for A != B where A and B are integers, use the absolute difference between A and B (that is: if 0 <= A-B then A-B else B-A)

-                    Expression AminusB = CreateIntSub(s.Tok, bin.E0, bin.E1);

-                    Expression BminusA = CreateIntSub(s.Tok, bin.E1, bin.E0);

-                    Expression zero = CreateIntLiteral(s.Tok, 0);

-                    BinaryExpr test = new BinaryExpr(s.Tok, BinaryExpr.Opcode.Le, zero, AminusB);

-                    test.ResolvedOp = BinaryExpr.ResolvedOpcode.Le;  // resolve here

-                    test.Type = Type.Bool;  // resolve here

-                    guess = CreateIntITE(s.Tok, test, AminusB, BminusA);

-                  }

-                  break;

-                default:

-                  break;

-              }

-            }

-            if (guess != null) {

-              if (prefix != null) {

-                // Make the following guess:  if prefix then guess else -1

-                Expression negativeOne = CreateIntLiteral(s.Tok, -1);

-                guess = CreateIntITE(s.Tok, prefix, guess, negativeOne);

-              }

-              theDecreases.Add(guess);

-              inferredDecreases = true;

-              break;  // ignore any further conjuncts

-            }

-            if (prefix == null) {

-              prefix = guardConjunct;

-            } else {

-              BinaryExpr and = new BinaryExpr(s.Tok, BinaryExpr.Opcode.And, prefix, guardConjunct);

-              and.ResolvedOp = BinaryExpr.ResolvedOpcode.And;  // resolve here

-              and.Type = Type.Bool;  // resolve here

-              prefix = and;

-            }

-          }

-        }

+        bool inferredDecreases;

+        List<Expression> theDecreases = LoopDecreasesWithDefault(s, out inferredDecreases);

         

         Bpl.LocalVariable preLoopHeapVar = new Bpl.LocalVariable(stmt.Tok, new Bpl.TypedIdent(stmt.Tok, "$PreLoopHeap" + loopId, predef.HeapType));

         locals.Add(preLoopHeapVar);

@@ -2687,8 +2903,10 @@ namespace Microsoft.Dafny {
         List<Bpl.PredicateCmd> invariants = new List<Bpl.PredicateCmd>();

         Bpl.StmtListBuilder invDefinednessBuilder = new Bpl.StmtListBuilder();

         foreach (MaybeFreeExpression loopInv in s.Invariants) {

-          invDefinednessBuilder.Add(AssertNS(loopInv.E.tok, IsTotal(loopInv.E, etran), (loopInv.IsFree ? "free " : "") + "loop invariant must be well defined"));  // totality check

+          TrStmt_CheckWellformed(loopInv.E, invDefinednessBuilder, locals, etran, false);

           invDefinednessBuilder.Add(new Bpl.AssumeCmd(loopInv.E.tok, etran.TrExpr(loopInv.E)));

+

+          invariants.Add(new Bpl.AssumeCmd(loopInv.E.tok, Bpl.Expr.Imp(w, CanCallAssumption(loopInv.E, etran))));

           if (loopInv.IsFree) {

             invariants.Add(new Bpl.AssumeCmd(loopInv.E.tok, Bpl.Expr.Imp(w, etran.TrExpr(loopInv.E))));

           } else {

@@ -2710,8 +2928,9 @@ namespace Microsoft.Dafny {
           }

         }

         // check definedness of decreases clause

+        // TODO: can this check be omitted if the decreases clause is inferred?

         foreach (Expression e in theDecreases) {

-          invDefinednessBuilder.Add(Assert(e.tok, IsTotal(e, etran), "decreases expression must be well defined at top of each loop iteration"));  // totality check

+          TrStmt_CheckWellformed(e, invDefinednessBuilder, locals, etran, true);

         }

         // include boilerplate invariants

         foreach (BoilerplateTriple tri in GetTwoStateBoilerplate(stmt.Tok, currentMethod, etranPreLoop, etran)) {

@@ -2741,19 +2960,18 @@ namespace Microsoft.Dafny {
         invDefinednessBuilder.Add(new Bpl.AssumeCmd(stmt.Tok, Bpl.Expr.False));

         loopBodyBuilder.Add(new Bpl.IfCmd(stmt.Tok, Bpl.Expr.Not(w), invDefinednessBuilder.Collect(stmt.Tok), null, null));

         // generate:  assert IsTotal(guard); if (!guard) { break; }

-        Bpl.Expr guard;

-        if (s.Guard == null) {

-          guard = null;

-        } else {

-          loopBodyBuilder.Add(Assert(s.Guard.tok, IsTotal(s.Guard, etran), "loop guard must be well defined"));  // totality check

-          Bpl.StmtListBuilder guardBreak = new Bpl.StmtListBuilder();

-          guardBreak.Add(new Bpl.BreakCmd(s.Guard.tok, null));

-          loopBodyBuilder.Add(new Bpl.IfCmd(s.Guard.tok, Bpl.Expr.Not(etran.TrExpr(s.Guard)), guardBreak.Collect(s.Guard.tok), null, null));

-          guard = Bpl.Expr.True;

+        Bpl.Expr guard = null;

+        if (s.Guard != null) {

+          TrStmt_CheckWellformed(s.Guard, loopBodyBuilder, locals, etran, true);

+          guard = Bpl.Expr.Not(etran.TrExpr(s.Guard));

         }

+        Bpl.StmtListBuilder guardBreak = new Bpl.StmtListBuilder();

+        guardBreak.Add(new Bpl.BreakCmd(s.Tok, null));

+        loopBodyBuilder.Add(new Bpl.IfCmd(s.Tok, guard, guardBreak.Collect(s.Tok), null, null));

+

         loopBodyBuilder.Add(CaptureState(stmt.Tok, "loop entered"));

         // termination checking

-        if (Contract.Exists(theDecreases,e=> e is WildcardExpr)) {

+        if (Contract.Exists(theDecreases, e => e is WildcardExpr)) {

           // omit termination checking for this loop

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

         } else {

@@ -2772,9 +2990,14 @@ namespace Microsoft.Dafny {
           Bpl.Expr decrCheck = DecreasesCheck(toks, types, decrs, oldBfs, etran, loopBodyBuilder, " at end of loop iteration", false);

           loopBodyBuilder.Add(Assert(stmt.Tok, decrCheck, inferredDecreases ? "cannot prove termination; try supplying a decreases clause for the loop" : "decreases expression might not decrease"));

         }

+        // Finally, assume the well-formedness of the invariant (which has been checked once and for all above), so that the check

+        // of invariant-maintenance can use the appropriate canCall predicates.

+        foreach (MaybeFreeExpression loopInv in s.Invariants) {

+          loopBodyBuilder.Add(new Bpl.AssumeCmd(loopInv.E.tok, CanCallAssumption(loopInv.E, etran)));

+        }

         Bpl.StmtList body = loopBodyBuilder.Collect(stmt.Tok);

 

-        builder.Add(new Bpl.WhileCmd(stmt.Tok, guard, invariants, body));

+        builder.Add(new Bpl.WhileCmd(stmt.Tok, Bpl.Expr.True, invariants, body));

         builder.Add(CaptureState(stmt.Tok, "loop exit"));

 

       } else if (stmt is ForeachStmt) {

@@ -2798,7 +3021,7 @@ namespace Microsoft.Dafny {
         Bpl.IdentifierExpr o = new Bpl.IdentifierExpr(stmt.Tok, oVar);

 

         // colection

-        builder.Add(Assert(s.Collection.tok, IsTotal(s.Collection, etran), "collection expression must be well defined"));

+        TrStmt_CheckWellformed(s.Collection, builder, locals, etran, true);

         Bpl.Expr oInS;

         if (s.Collection.Type is SetType) {

           oInS = etran.TrInSet(stmt.Tok, o, s.Collection, ((SetType)s.Collection.Type).Arg);

@@ -2902,7 +3125,7 @@ namespace Microsoft.Dafny {
         

       } else if (stmt is MatchStmt) {

         MatchStmt s = (MatchStmt)stmt;

-        builder.Add(Assert(s.Source.tok, IsTotal(s.Source, etran), "match source expression must be well defined"));  // totality check

+        TrStmt_CheckWellformed(s.Source, builder, locals, etran, true);

         Bpl.Expr source = etran.TrExpr(s.Source);

         

         Bpl.StmtListBuilder b = new Bpl.StmtListBuilder();

@@ -2912,30 +3135,25 @@ namespace Microsoft.Dafny {
         for (int i = s.Cases.Count; 0 <= --i; ) {

           MatchCaseStmt mc = (MatchCaseStmt)s.Cases[i];

           // havoc all bound variables

-          List<Expression> rArgs = new List<Expression>();

-          Bpl.IdentifierExprSeq havocIds = new Bpl.IdentifierExprSeq();

-          foreach (BoundVar arg in mc.Arguments) {

-            Bpl.LocalVariable v = new Bpl.LocalVariable(arg.tok, new Bpl.TypedIdent(arg.tok, arg.UniqueName, TrType(arg.Type)));

-            locals.Add(v);

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

-            IdentifierExpr ie = new IdentifierExpr(arg.tok, arg.UniqueName);

-            ie.Var = arg;  ie.Type = ie.Var.Type;  // resolve it here

-            rArgs.Add(ie);

-          }

-          if (havocIds.Length != 0) {

+          b = new Bpl.StmtListBuilder();

+          VariableSeq newLocals = new VariableSeq();

+          Bpl.Expr r = CtorInvocation(mc, etran, newLocals, b);

+          locals.AddRange(newLocals);

+

+          if (newLocals.Length != 0) {

+            Bpl.IdentifierExprSeq havocIds = new Bpl.IdentifierExprSeq();

+            foreach (Variable local in newLocals) {

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

+            }

             builder.Add(new Bpl.HavocCmd(mc.tok, havocIds));

           }

-          Contract.Assert(mc.Ctor != null && mc.Ctor.EnclosingDatatype != null);  // everything has been successfully resolved

-          DatatypeValue r = new DatatypeValue(mc.tok, mc.Ctor.EnclosingDatatype.Name, mc.Ctor.Name, rArgs);

-          r.Ctor = mc.Ctor;  r.Type = new UserDefinedType(mc.tok, mc.Ctor.EnclosingDatatype.Name, new List<Type>()/*this is not right, but it seems like it won't matter here*/);  // resolve it here

 

           // translate the body into b

-          b = new Bpl.StmtListBuilder();

           foreach (Statement ss in mc.Body) {

             TrStmt(ss, b, locals, etran);

           }

 

-          Bpl.Expr guard = Bpl.Expr.Eq(source, etran.TrExpr(r));

+          Bpl.Expr guard = Bpl.Expr.Eq(source, r);

           ifCmd = new Bpl.IfCmd(mc.tok, guard, b.Collect(mc.tok), ifCmd, els);

           els = null;

         }

@@ -3224,71 +3442,84 @@ namespace Microsoft.Dafny {
     }    

     

     Bpl.Expr GetWhereClause(IToken tok, Bpl.Expr x, Type type, ExpressionTranslator etran)

-     {

+    {

       Contract.Requires(tok != null);

       Contract.Requires(x != null);

       Contract.Requires(type != null);

       Contract.Requires(etran != null);

       Contract.Requires(predef != null);

-      if (type is TypeProxy) {

-        // unresolved proxy

-        Contract.Assert(((TypeProxy)type).T == null);

-        // omit where clause (in other places, unresolved proxies are treated as a reference type; we could do that here too, but

-        // we might as well leave out the where clause altogether)

-        return null;

-      } else if (type is BoolType || type is IntType) {

-        return null;

+      while (true) {

+        TypeProxy proxy = type as TypeProxy;

+        if (proxy == null) {

+          break;

+        } else if (proxy.T == null) {

+          // Unresolved proxy

+          // Omit where clause (in other places, unresolved proxies are treated as a reference type; we could do that here too, but

+          // we might as well leave out the where clause altogether).

+          return null;

+        } else {

+          type = proxy.T;

+        }

+      }

+

+      if (type is BoolType || type is IntType) {

+        // nothing todo

+      

       } else if (type is SetType) {

         SetType st = (SetType)type;

-        if (st.Arg.IsRefType) {

-          // (forall t: BoxType :: { x[t] } x[t] ==> Unbox(t) == null || $Heap[Unbox(t),alloc])

-          Bpl.BoundVariable tVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$t", predef.BoxType));

-          Bpl.Expr t = new Bpl.IdentifierExpr(tok, tVar);

-          Bpl.Expr xSubT = Bpl.Expr.SelectTok(tok, x, t);

-          Bpl.Expr unboxT = FunctionCall(tok, BuiltinFunction.Unbox, predef.RefType, t);

-

+        // (forall t: BoxType :: { x[t] } x[t] ==> Unbox(t)-has-the-expected-type)

+        Bpl.BoundVariable tVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$t#" + otherTmpVarCount, predef.BoxType));

+        otherTmpVarCount++;

+        Bpl.Expr t = new Bpl.IdentifierExpr(tok, tVar);

+        Bpl.Expr xSubT = Bpl.Expr.SelectTok(tok, x, t);

+        Bpl.Expr unboxT = ExpressionTranslator.ModeledAsBoxType(st.Arg) ? t : FunctionCall(tok, BuiltinFunction.Unbox, TrType(st.Arg), t);

+

+        Bpl.Expr wh = GetWhereClause(tok, unboxT, st.Arg, etran);

+        if (wh != null) {

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

-          

-          Bpl.Expr goodRef = etran.GoodRef(tok, unboxT, st.Arg);

-          Bpl.Expr body = Bpl.Expr.Imp(xSubT, Bpl.Expr.Or(Bpl.Expr.Eq(unboxT, predef.Null), goodRef));

-          return new Bpl.ForallExpr(tok, new Bpl.VariableSeq(tVar), tr, body);

-        } else {

-          // TODO:  should also handle sets of sets, etc.

-          return null;

+          return new Bpl.ForallExpr(tok, new Bpl.VariableSeq(tVar), tr, Bpl.Expr.Imp(xSubT, wh));

         }

         

       } else if (type is SeqType) {

         SeqType st = (SeqType)type;

-        if (st.Arg.IsRefType) {

-          // (forall i: int :: { Seq#Index(x,i) }

-          //      0 <= i && i < Seq#Length(x) ==> Unbox(Seq#Index(x,i)) == null || $Heap[Unbox(Seq#Index(x,i)), alloc])

-          Bpl.BoundVariable iVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$i", Bpl.Type.Int));

-          Bpl.Expr i = new Bpl.IdentifierExpr(tok, iVar);

-          Bpl.Expr xSubI = FunctionCall(tok, BuiltinFunction.SeqIndex, predef.BoxType, x, i);

-          Bpl.Expr unbox = FunctionCall(tok, BuiltinFunction.Unbox, predef.RefType, xSubI);

-

+        // (forall i: int :: { Seq#Index(x,i) }

+        //      0 <= i && i < Seq#Length(x) ==> Unbox(Seq#Index(x,i))-has-the-expected-type)

+        Bpl.BoundVariable iVar = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$i#" + otherTmpVarCount, Bpl.Type.Int));

+        otherTmpVarCount++;

+        Bpl.Expr i = new Bpl.IdentifierExpr(tok, iVar);

+        Bpl.Expr xSubI = FunctionCall(tok, BuiltinFunction.SeqIndex, predef.BoxType, x, i);

+        Bpl.Expr unbox = ExpressionTranslator.ModeledAsBoxType(st.Arg) ? xSubI : FunctionCall(tok, BuiltinFunction.Unbox, TrType(st.Arg), xSubI);

+

+        Bpl.Expr wh = GetWhereClause(tok, unbox, st.Arg, etran);

+        if (wh != null) {

           Bpl.Expr range = InSeqRange(tok, i, x, true, null, false);

-

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

-

-          Bpl.Expr goodRef = etran.GoodRef(tok, unbox, st.Arg);

-          Bpl.Expr body = Bpl.Expr.Imp(range, Bpl.Expr.Or(Bpl.Expr.Eq(unbox, predef.Null), goodRef));

-          return new Bpl.ForallExpr(tok, new Bpl.VariableSeq(iVar), tr, body);

-        } else {

-          // TODO: should also handle sequences or sequences, etc.

-          return null;

+          return new Bpl.ForallExpr(tok, new Bpl.VariableSeq(iVar), tr, Bpl.Expr.Imp(range, wh));

         }

 

       } else if (type.IsRefType) {

         // reference type:

-        // x == null || $Heap[x,alloc]

+        // x == null || ($Heap[x,alloc] && dtype(x) == ...)

         return Bpl.Expr.Or(Bpl.Expr.Eq(x, predef.Null), etran.GoodRef(tok, x, type));

+

+      } else if (type.IsDatatype) {

+        UserDefinedType udt = (UserDefinedType)type;

+

+        // DtAlloc(e, heap) && e-has-the-expected-type

+        Bpl.Expr alloc = FunctionCall(tok, BuiltinFunction.DtAlloc, null, x, etran.HeapExpr);

+        Bpl.Expr goodType = etran.Good_Datatype(tok, x, udt.ResolvedClass, udt.TypeArgs);

+        return Bpl.Expr.And(alloc, goodType);

+

+      } else if (type.IsTypeParameter) {

+        return FunctionCall(tok, BuiltinFunction.GenericAlloc, null, x, etran.HeapExpr);

+        

       } else {

-        // type parameter

-        return null;

+        Contract.Assert(false); throw new cce.UnreachableException();  // unexpected type

       }

+

+      return null;

     }

-    

+

     void TrAssignment(IToken tok, Expression lhs, AssignmentRhs rhs, Bpl.StmtListBuilder builder, Bpl.VariableSeq locals,

                       ExpressionTranslator etran)

     {

@@ -3300,8 +3531,8 @@ namespace Microsoft.Dafny {
       Contract.Requires(etran != null);

       Contract.Requires(predef != null);

       if (rhs is ExprRhs) {

-        builder.Add(Assert(tok, IsTotal(lhs, etran), "LHS expression must be well defined"));  // totality check

-        builder.Add(Assert(tok, IsTotal(((ExprRhs)rhs).Expr, etran), "RHS expression must be well defined"));  // totality check

+        TrStmt_CheckWellformed(lhs, builder, locals, etran, true);

+        TrStmt_CheckWellformed(((ExprRhs)rhs).Expr, builder, locals, etran, true);

         Bpl.Expr bRhs = etran.TrExpr(((ExprRhs)rhs).Expr);

         if (lhs is IdentifierExpr) {

           Bpl.IdentifierExpr bLhs = (Bpl.IdentifierExpr)etran.TrExpr(lhs);  // TODO: is this cast always justified?

@@ -3506,6 +3737,12 @@ namespace Microsoft.Dafny {
           return oldEtran;

         }

       }

+

+      public bool UsesOldHeap {

+        get {

+          return HeapExpr is Bpl.OldExpr;

+        }

+      }

       

       public ExpressionTranslator LimitedFunctions(Function applyLimited_CurrentFunction) {

         Contract.Requires(applyLimited_CurrentFunction != null);

@@ -3718,7 +3955,12 @@ namespace Microsoft.Dafny {
             Bpl.Expr oIsFresh = Bpl.Expr.Not(IsAlloced(expr.tok, TrExpr(e.E), oldHeap));

             return Bpl.Expr.Or(oNull, oIsFresh);

           }

-        

+

+        } else if (expr is AllocatedExpr) {

+          AllocatedExpr e = (AllocatedExpr)expr;

+          Bpl.Expr wh = translator.GetWhereClause(e.tok, TrExpr(e.E), e.E.Type, this);

+          return wh == null ? Bpl.Expr.True : wh;

+

         } else if (expr is UnaryExpr) {

           UnaryExpr e = (UnaryExpr)expr;

           Bpl.Expr arg = TrExpr(e.E);

@@ -3844,9 +4086,7 @@ namespace Microsoft.Dafny {
         } else if (expr is QuantifierExpr) {

           QuantifierExpr e = (QuantifierExpr)expr;

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

-          foreach (BoundVar bv in e.BoundVars) {

-            bvars.Add(new Bpl.BoundVariable(bv.tok, new Bpl.TypedIdent(bv.tok, bv.UniqueName, translator.TrType(bv.Type))));

-          }

+          Bpl.Expr typeAntecedent = TrBoundVariables(e, bvars);

           Bpl.QKeyValue kv = TrAttributes(e.Attributes);

           Bpl.Trigger tr = null;

           for (Triggers trigs = e.Trigs; trigs != null; trigs = trigs.Prev) {

@@ -3859,10 +4099,10 @@ namespace Microsoft.Dafny {
           Bpl.Expr body = TrExpr(e.Body);

           

           if (e is ForallExpr) {

-            return new Bpl.ForallExpr(expr.tok, new Bpl.TypeVariableSeq(), bvars, kv, tr, body);

+            return new Bpl.ForallExpr(expr.tok, new Bpl.TypeVariableSeq(), bvars, kv, tr, Bpl.Expr.Imp(typeAntecedent, body));

           } else {

             Contract.Assert(e is ExistsExpr);

-            return new Bpl.ExistsExpr(expr.tok, new Bpl.TypeVariableSeq(), bvars, kv, tr, body);

+            return new Bpl.ExistsExpr(expr.tok, new Bpl.TypeVariableSeq(), bvars, kv, tr, Bpl.Expr.And(typeAntecedent, body));

           }

         

         } else if (expr is ITEExpr) {

@@ -3885,6 +4125,22 @@ namespace Microsoft.Dafny {
         }

       }

 

+      public Bpl.Expr TrBoundVariables(QuantifierExpr e, Bpl.VariableSeq bvars) {

+        Contract.Requires(e != null);

+        Contract.Ensures(Contract.Result<Bpl.Expr>() != null);

+        

+        Bpl.Expr typeAntecedent = Bpl.Expr.True;

+        foreach (BoundVar bv in e.BoundVars) {

+          Bpl.Variable bvar = new Bpl.BoundVariable(bv.tok, new Bpl.TypedIdent(bv.tok, bv.UniqueName, translator.TrType(bv.Type)));

+          bvars.Add(bvar);

+          Bpl.Expr wh = translator.GetWhereClause(bv.tok, new Bpl.IdentifierExpr(bv.tok, bvar), bv.Type, this);

+          if (wh != null) {

+            typeAntecedent = translator.BplAnd(typeAntecedent, wh);

+          }

+        }

+        return typeAntecedent;

+      }

+

       public ExprSeq FunctionInvocationArguments(FunctionCallExpr e) {

         Contract.Requires(e != null);

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

@@ -3996,12 +4252,12 @@ namespace Microsoft.Dafny {
         Contract.Requires(fromType != null);

         Contract.Requires(toType != null);

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

+

         if (ModeledAsBoxType(fromType) && !ModeledAsBoxType(toType)) {

           return translator.FunctionCall(tok, BuiltinFunction.Unbox, translator.TrType(toType), e);

         } else {

           return e;

         }

-      

       }

       

       public static bool ModeledAsBoxType(Type t) {

@@ -4167,12 +4423,13 @@ namespace Microsoft.Dafny {
         Contract.Ensures(Contract.Result<Bpl.Expr>() != null);

         return GoodRef_Ref(tok, e, new Bpl.IdentifierExpr(tok, translator.GetClass(type.ResolvedClass)), type.TypeArgs, isNew);

       }

-      

+

       public Bpl.Expr GoodRef_Ref(IToken tok, Bpl.Expr e, Bpl.Expr type, List<Type/*!*/>/*!*/ typeArgs, bool isNew) {

         Contract.Requires(tok != null);

         Contract.Requires(e != null);

         Contract.Requires(type != null);

         Contract.Requires(cce.NonNullElements(typeArgs));

+

         // Heap[e, alloc]

         Bpl.Expr r = IsAlloced(tok, e);

         if (isNew) {

@@ -4182,9 +4439,9 @@ namespace Microsoft.Dafny {
         // dtype(e) == C

         Bpl.Expr dtypeFunc = translator.FunctionCall(tok, BuiltinFunction.DynamicType, null, e);

         Bpl.Expr dtype = Bpl.Expr.Eq(dtypeFunc, type);

-        r = Bpl.Expr.And(r, dtype);

+        r = r == null ? dtype : Bpl.Expr.And(r, dtype);

         

-        // dtypeParams(e, #) == T

+        // TypeParams(e, #) == T

         int n = 0;

         foreach (Type arg in typeArgs) {

           Bpl.Expr tpFunc = translator.FunctionCall(tok, BuiltinFunction.TypeParams, null, e, Bpl.Expr.Literal(n));

@@ -4197,52 +4454,28 @@ namespace Microsoft.Dafny {
         

         return r;

       }

-      

-      public Bpl.Expr TypeAlloced(IToken tok, Bpl.Expr e, Type type) {

+

+      public Bpl.Expr Good_Datatype(IToken tok, Bpl.Expr e, TopLevelDecl resolvedClass, List<Type> typeArgs) {

         Contract.Requires(tok != null);

-        Contract.Requires(e!= null);

-        Contract.Requires(type != null);

-        while (true) {

-          TypeProxy proxy = type as TypeProxy;

-          if (proxy == null) {

-            break;

-          } else if (proxy.T == null) {

-            return null;

-          } else {

-            type = proxy.T;

+        Contract.Requires(e != null);

+        Contract.Requires(resolvedClass != null);

+        Contract.Requires(typeArgs != null);

+

+        // DtType(e) == C

+        Bpl.Expr dttypeFunc = translator.FunctionCall(tok, BuiltinFunction.DtType, null, e);

+        Bpl.Expr r = Bpl.Expr.Eq(dttypeFunc, new Bpl.IdentifierExpr(tok, translator.GetClass(resolvedClass)));

+

+        // DtTypeParams(e, #) == T

+        int n = 0;

+        foreach (Type arg in typeArgs) {

+          Bpl.Expr tpFunc = translator.FunctionCall(tok, BuiltinFunction.DtTypeParams, null, e, Bpl.Expr.Literal(n));

+          Bpl.Expr ta = translator.GetTypeExpr(tok, arg);

+          if (ta != null) {

+            r = Bpl.Expr.And(r, Bpl.Expr.Eq(tpFunc, ta));

           }

+          n++;

         }

-        

-        Bpl.BoundVariable bv = null;

-        Bpl.Expr ante = null;

-        if (type.IsRefType) {  // object or class type

-          // e == null || $Heap[e, alloc]

-          // This is done below

-          

-        } else if (type is SetType) {

-          // (forall tp: BoxType :: e[tp] ==> Unbox(tp) == null || $Heap[Unbox(tp), alloc])

-          bv = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$tp", predef.BoxType));

-          Bpl.Expr tp = new Bpl.IdentifierExpr(tok, bv);

-          ante = Bpl.Expr.SelectTok(tok, e, tp);  // note, this means the set-inclusion does not undergo the set-inclusion expansion optimization done by TrInSet

-          e = translator.FunctionCall(tok, BuiltinFunction.Unbox, predef.RefType, tp);

-          

-        } else if (type is SeqType) {

-          // (forall i: int :: Unbox(Seq#Index(e,i)) == null || $Heap[Unbox(Seq#Index(e,i)), alloc])

-          bv = new Bpl.BoundVariable(tok, new Bpl.TypedIdent(tok, "$i", Bpl.Type.Int));

-          e = translator.FunctionCall(tok, BuiltinFunction.SeqIndex, predef.BoxType, e, new Bpl.IdentifierExpr(tok, bv));

-          e = translator.FunctionCall(tok, BuiltinFunction.Unbox, predef.RefType, e);

-          

-        } else {

-          return null;

-        }

-        

-        Bpl.Expr r = Bpl.Expr.Or(Bpl.Expr.Eq(e, predef.Null), GoodRef(tok, e, type));

-        if (ante != null) {

-          r = Bpl.Expr.Imp(ante, r);

-        }

-        if (bv != null) {

-          r = new Bpl.ForallExpr(tok, new Bpl.VariableSeq(bv), r);

-        }

+

         return r;

       }

     }

@@ -4278,14 +4511,19 @@ namespace Microsoft.Dafny {
       IsGoodHeap,

       HeapSucc,

       

-      DynamicType,  // allocated type

-      TypeParams,   // type parameters to allocated type

+      DynamicType,  // allocated type (of object reference)

+      DtType,       // type of datatype value

+      TypeParams,   // type parameters of allocated type

+      DtTypeParams, // type parameters of datatype

       TypeTuple,

       DeclType,

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

-      

+

       DatatypeCtorId,

-      DtRank

+      DtRank,

+      DtAlloc,

+

+      GenericAlloc,

     }

     

     // The "typeInstantiation" argument is passed in to help construct the result type of the function.

@@ -4410,10 +4648,18 @@ namespace Microsoft.Dafny {
           Contract.Assert(args.Length == 1);

           Contract.Assert(typeInstantiation == null);

           return FunctionCall(tok, "dtype", predef.ClassNameType, args);

+        case BuiltinFunction.DtType:

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

+          Contract.Assert(typeInstantiation == null);

+          return FunctionCall(tok, "DtType", predef.ClassNameType, args);

         case BuiltinFunction.TypeParams:

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

           Contract.Assert(typeInstantiation == null);

           return FunctionCall(tok, "TypeParams", predef.ClassNameType, args);

+        case BuiltinFunction.DtTypeParams:

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

+          Contract.Assert(typeInstantiation == null);

+          return FunctionCall(tok, "DtTypeParams", predef.ClassNameType, args);

         case BuiltinFunction.TypeTuple:

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

           Contract.Assert(typeInstantiation == null);

@@ -4426,7 +4672,7 @@ namespace Microsoft.Dafny {
           Contract.Assert(args.Length == 1);

           Contract.Assert(typeInstantiation != null);

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

-          

+

         case BuiltinFunction.DatatypeCtorId:

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

           Contract.Assert(typeInstantiation == null);

@@ -4435,7 +4681,16 @@ namespace Microsoft.Dafny {
           Contract.Assert(args.Length == 1);

           Contract.Assert(typeInstantiation == null);

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

-          

+        case BuiltinFunction.DtAlloc:

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

+          Contract.Assert(typeInstantiation == null);

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

+

+        case BuiltinFunction.GenericAlloc:

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

+          Contract.Assert(typeInstantiation == null);

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

+

         default:

           Contract.Assert(false); throw new cce.UnreachableException();  // unexpected built-in function

       }

@@ -4700,6 +4955,12 @@ namespace Microsoft.Dafny {
         if (se != e.E) {

           newExpr = new FreshExpr(expr.tok, se);

         }

+      } else if (expr is AllocatedExpr) {

+        AllocatedExpr e = (AllocatedExpr)expr;

+        Expression se = Substitute(e.E, receiverReplacement, substMap);

+        if (se != e.E) {

+          newExpr = new AllocatedExpr(expr.tok, se);

+        }

       } else if (expr is UnaryExpr) {

         UnaryExpr e = (UnaryExpr)expr;

         Expression se = Substitute(e.E, receiverReplacement, substMap);

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 4307319f..931c7d62 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -82,7 +82,7 @@ TypeTests.dfy(72,6): Error: Duplicate local-variable name: y
 14 resolution/type errors detected in TypeTests.dfy

 

 -------------------- SmallTests.dfy --------------------

-SmallTests.dfy(30,7): Error: RHS expression must be well defined

+SmallTests.dfy(30,11): Error: index out of range

 Execution trace:

     (0,0): anon0

 SmallTests.dfy(61,36): Error: possible division by zero

@@ -99,12 +99,12 @@ Execution trace:
     (0,0): anon3

     (0,0): anon13_Then

     (0,0): anon6

-SmallTests.dfy(82,20): Error: decreases expression must be well defined at top of each loop iteration

+SmallTests.dfy(82,24): Error: target object may be null

 Execution trace:

     (0,0): anon0

-    SmallTests.dfy(81,5): anon7_LoopHead

-    (0,0): anon7_LoopBody

-    (0,0): anon8_Then

+    SmallTests.dfy(81,5): anon9_LoopHead

+    (0,0): anon9_LoopBody

+    (0,0): anon10_Then

 SmallTests.dfy(116,5): Error: call may violate caller's modifies clause

 Execution trace:

     (0,0): anon0

@@ -123,8 +123,27 @@ Execution trace:
     (0,0): anon0

     (0,0): anon4_Else

     (0,0): anon3

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

+Execution trace:

+    (0,0): anon0

+    (0,0): anon12_Then

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

+Execution trace:

+    (0,0): anon0

+    (0,0): anon12_Else

+    (0,0): anon3

+    (0,0): anon13_Then

+SmallTests.dfy(226,12): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon12_Else

+    (0,0): anon3

+    (0,0): anon13_Else

+    (0,0): anon6

+    (0,0): anon14_Then

+    (0,0): anon11

 

-Dafny program verifier finished with 28 verified, 9 errors

+Dafny program verifier finished with 29 verified, 12 errors

 

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

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

@@ -152,38 +171,41 @@ Execution trace:
 Definedness.dfy(55,18): Error: target object may be null

 Execution trace:

     (0,0): anon0

-Definedness.dfy(77,9): Error: LHS expression must be well defined

+Definedness.dfy(77,7): Error: target object may be null

+Execution trace:

+    (0,0): anon0

+Definedness.dfy(78,5): Error: possible violation of function precondition

 Execution trace:

     (0,0): anon0

-Definedness.dfy(78,12): Error: LHS expression must be well defined

+Definedness.dfy(79,10): Error: possible violation of function precondition

 Execution trace:

     (0,0): anon0

-Definedness.dfy(79,7): Error: RHS expression must be well defined

+Definedness.dfy(84,14): Error: possible division by zero

 Execution trace:

     (0,0): anon0

-Definedness.dfy(84,18): Error: assert condition must be well defined

+Definedness.dfy(84,23): Error: possible division by zero

 Execution trace:

     (0,0): anon0

-Definedness.dfy(85,5): Error: assume condition must be well defined

+Definedness.dfy(85,15): Error: possible division by zero

 Execution trace:

     (0,0): anon0

-Definedness.dfy(90,16): Error: if guard must be well defined

+Definedness.dfy(90,12): Error: possible division by zero

 Execution trace:

     (0,0): anon0

-Definedness.dfy(97,19): Error: loop guard must be well defined

+Definedness.dfy(97,15): Error: possible division by zero

 Execution trace:

     (0,0): anon0

     Definedness.dfy(97,5): anon8_LoopHead

     (0,0): anon8_LoopBody

     Definedness.dfy(97,5): anon9_Else

     (0,0): anon3

-Definedness.dfy(106,23): Error: decreases expression must be well defined at top of each loop iteration

+Definedness.dfy(106,23): Error: possible violation of function precondition

 Execution trace:

     (0,0): anon0

     Definedness.dfy(105,5): anon13_LoopHead

     (0,0): anon13_LoopBody

     (0,0): anon14_Then

-Definedness.dfy(112,17): Error: decreases expression must be well defined at top of each loop iteration

+Definedness.dfy(112,17): Error: possible violation of function precondition

 Execution trace:

     (0,0): anon0

     Definedness.dfy(105,5): anon13_LoopHead

@@ -195,7 +217,7 @@ Execution trace:
     Definedness.dfy(111,5): anon16_LoopHead

     (0,0): anon16_LoopBody

     (0,0): anon17_Then

-Definedness.dfy(122,22): Error: loop invariant must be well defined

+Definedness.dfy(122,17): Error: possible violation of function precondition

 Execution trace:

     (0,0): anon0

     Definedness.dfy(121,5): anon7_LoopHead

@@ -204,45 +226,49 @@ Execution trace:
 Definedness.dfy(122,22): Error BP5004: This loop invariant might not hold on entry.

 Execution trace:

     (0,0): anon0

-Definedness.dfy(123,17): Error: decreases expression must be well defined at top of each loop iteration

+Definedness.dfy(123,17): Error: possible violation of function precondition

 Execution trace:

     (0,0): anon0

     Definedness.dfy(121,5): anon7_LoopHead

     (0,0): anon7_LoopBody

     (0,0): anon8_Then

-Definedness.dfy(132,24): Error: loop guard must be well defined

+Definedness.dfy(132,15): Error: possible division by zero

 Execution trace:

     (0,0): anon0

-    Definedness.dfy(132,5): anon7_LoopHead

-    (0,0): anon7_LoopBody

-    Definedness.dfy(132,5): anon8_Else

+    Definedness.dfy(132,5): anon9_LoopHead

+    (0,0): anon9_LoopBody

+    Definedness.dfy(132,5): anon10_Else

     (0,0): anon3

-Definedness.dfy(151,24): Error: loop guard must be well defined

+Definedness.dfy(151,15): Error: possible division by zero

 Execution trace:

     (0,0): anon0

-    Definedness.dfy(145,5): anon13_LoopHead

-    (0,0): anon13_LoopBody

-    Definedness.dfy(145,5): anon14_Else

+    Definedness.dfy(145,5): anon17_LoopHead

+    (0,0): anon17_LoopBody

+    Definedness.dfy(145,5): anon18_Else

     (0,0): anon3

-    (0,0): anon15_Then

-    (0,0): anon6

-    Definedness.dfy(151,5): anon16_LoopHead

-    (0,0): anon16_LoopBody

-    Definedness.dfy(151,5): anon17_Else

-    (0,0): anon9

-Definedness.dfy(170,44): Error: loop invariant must be well defined

+    (0,0): anon19_Then

+    (0,0): anon5

+    (0,0): anon20_Then

+    (0,0): anon8

+    Definedness.dfy(151,5): anon21_LoopHead

+    (0,0): anon21_LoopBody

+    Definedness.dfy(151,5): anon22_Else

+    (0,0): anon11

+Definedness.dfy(170,17): Error: possible violation of function precondition

 Execution trace:

     (0,0): anon0

-    Definedness.dfy(162,5): anon16_LoopHead

-    (0,0): anon16_LoopBody

-    Definedness.dfy(162,5): anon17_Else

+    Definedness.dfy(162,5): anon19_LoopHead

+    (0,0): anon19_LoopBody

+    Definedness.dfy(162,5): anon20_Else

     (0,0): anon3

-    (0,0): anon18_Then

+    (0,0): anon21_Then

     (0,0): anon6

-    Definedness.dfy(169,5): anon19_LoopHead

-    (0,0): anon19_LoopBody

-    (0,0): anon20_Then

-Definedness.dfy(191,21): Error: collection expression must be well defined

+    Definedness.dfy(169,5): anon22_LoopHead

+    (0,0): anon22_LoopBody

+    (0,0): anon23_Then

+    (0,0): anon24_Then

+    (0,0): anon11

+Definedness.dfy(191,24): Error: possible violation of function precondition

 Execution trace:

     (0,0): anon0

 Definedness.dfy(193,11): Error: foreach assignment may update an object not in the enclosing method's modifies clause

@@ -254,7 +280,7 @@ Execution trace:
 Definedness.dfy(201,18): Error: RHS of assignment must be well defined

 Execution trace:

     (0,0): anon0

-Definedness.dfy(210,23): Error: loop invariant must be well defined

+Definedness.dfy(210,19): Error: possible division by zero

 Execution trace:

     (0,0): anon0

     Definedness.dfy(208,5): anon7_LoopHead

@@ -263,6 +289,12 @@ Execution trace:
 Definedness.dfy(210,23): Error BP5004: This loop invariant might not hold on entry.

 Execution trace:

     (0,0): anon0

+Definedness.dfy(210,28): Error: possible division by zero

+Execution trace:

+    (0,0): anon0

+    Definedness.dfy(208,5): anon7_LoopHead

+    (0,0): anon7_LoopBody

+    (0,0): anon8_Then

 Definedness.dfy(231,30): Error: possible violation of function postcondition

 Execution trace:

     (0,0): anon0

@@ -278,7 +310,7 @@ Execution trace:
     (0,0): anon2

     (0,0): anon8_Else

 

-Dafny program verifier finished with 23 verified, 32 errors

+Dafny program verifier finished with 23 verified, 34 errors

 

 -------------------- FunctionSpecifications.dfy --------------------

 FunctionSpecifications.dfy(31,13): Error: possible violation of function postcondition

@@ -307,11 +339,13 @@ Dafny program verifier finished with 3 verified, 3 errors
 Array.dfy(10,12): Error: assignment may update an array element not in the enclosing method's modifies clause

 Execution trace:

     (0,0): anon0

-    (0,0): anon3_Then

-Array.dfy(17,9): Error: RHS expression must be well defined

+    (0,0): anon5_Then

+    (0,0): anon2

+    (0,0): anon6_Then

+Array.dfy(17,16): Error: target object may be null

 Execution trace:

     (0,0): anon0

-Array.dfy(24,10): Error: LHS expression must be well defined

+Array.dfy(24,6): Error: index out of range

 Execution trace:

     (0,0): anon0

 Array.dfy(48,20): Error: assertion violation

@@ -320,11 +354,15 @@ Execution trace:
 Array.dfy(56,12): Error: assignment may update an array element not in the enclosing method's modifies clause

 Execution trace:

     (0,0): anon0

-    (0,0): anon3_Then

+    (0,0): anon5_Then

+    (0,0): anon2

+    (0,0): anon6_Then

 Array.dfy(63,12): Error: assignment may update an array element not in the enclosing method's modifies clause

 Execution trace:

     (0,0): anon0

-    (0,0): anon3_Then

+    (0,0): anon5_Then

+    (0,0): anon2

+    (0,0): anon6_Then

 Array.dfy(95,18): Error: assertion violation

 Execution trace:

     (0,0): anon0

@@ -351,8 +389,8 @@ Dafny program verifier finished with 22 verified, 11 errors
 MultiDimArray.dfy(53,21): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    (0,0): anon9_Then

-    (0,0): anon10_Then

+    (0,0): anon11_Then

+    (0,0): anon12_Then

 MultiDimArray.dfy(80,25): Error: assertion violation

 Execution trace:

     (0,0): anon0

@@ -397,42 +435,54 @@ Execution trace:
     (0,0): anon7_LoopBody

     Termination.dfy(102,3): anon8_Else

     (0,0): anon3

-    Termination.dfy(102,12): anon9_Else

+    Termination.dfy(102,3): anon9_Else

     (0,0): anon5

 Termination.dfy(110,3): Error: cannot prove termination; try supplying a decreases clause for the loop

 Execution trace:

     (0,0): anon0

-    Termination.dfy(110,3): anon7_LoopHead

-    (0,0): anon7_LoopBody

-    Termination.dfy(110,3): anon8_Else

-    (0,0): anon3

-    Termination.dfy(110,16): anon9_Else

+    Termination.dfy(110,3): anon9_LoopHead

+    (0,0): anon9_LoopBody

+    Termination.dfy(110,3): anon10_Else

+    (0,0): anon11_Then

     (0,0): anon5

+    Termination.dfy(110,3): anon12_Else

+    (0,0): anon7

 Termination.dfy(119,3): Error: decreases expression might not decrease

 Execution trace:

     (0,0): anon0

-    Termination.dfy(119,3): anon7_LoopHead

-    (0,0): anon7_LoopBody

-    Termination.dfy(119,3): anon8_Else

-    (0,0): anon3

-    Termination.dfy(119,16): anon9_Else

+    Termination.dfy(119,3): anon9_LoopHead

+    (0,0): anon9_LoopBody

+    Termination.dfy(119,3): anon10_Else

+    (0,0): anon11_Then

     (0,0): anon5

+    Termination.dfy(119,3): anon12_Else

+    (0,0): anon7

 Termination.dfy(120,17): Error: decreases expression must be bounded below by 0 at end of loop iteration

 Execution trace:

     (0,0): anon0

-    Termination.dfy(119,3): anon7_LoopHead

-    (0,0): anon7_LoopBody

-    Termination.dfy(119,3): anon8_Else

-    (0,0): anon3

-    Termination.dfy(119,16): anon9_Else

+    Termination.dfy(119,3): anon9_LoopHead

+    (0,0): anon9_LoopBody

+    Termination.dfy(119,3): anon10_Else

+    (0,0): anon11_Then

     (0,0): anon5

+    Termination.dfy(119,3): anon12_Else

+    (0,0): anon7

 Termination.dfy(248,36): Error: cannot prove termination; try supplying a decreases clause

 Execution trace:

     (0,0): anon6_Else

     (0,0): anon7_Else

     (0,0): anon8_Then

+Termination.dfy(288,3): Error: decreases expression might not decrease

+Execution trace:

+    (0,0): anon0

+    Termination.dfy(288,3): anon10_LoopHead

+    (0,0): anon10_LoopBody

+    Termination.dfy(288,3): anon11_Else

+    Termination.dfy(288,3): anon12_Else

+    (0,0): anon13_Else

+    (0,0): anon8

 

-Dafny program verifier finished with 35 verified, 5 errors

+Dafny program verifier finished with 41 verified, 6 errors

 

 -------------------- Use.dfy --------------------

 Use.dfy(16,18): Error: assertion violation

@@ -472,14 +522,11 @@ Dafny program verifier finished with 39 verified, 10 errors
 DTypes.dfy(15,14): Error: assertion violation

 Execution trace:

     (0,0): anon0

-DTypes.dfy(28,13): Error: assertion violation

-Execution trace:

-    (0,0): anon0

-DTypes.dfy(54,18): Error: assertion violation

+DTypes.dfy(53,18): Error: assertion violation

 Execution trace:

     (0,0): anon0

 

-Dafny program verifier finished with 14 verified, 3 errors

+Dafny program verifier finished with 15 verified, 2 errors

 

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

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

@@ -488,20 +535,62 @@ Execution trace:
 TypeParameters.dfy(63,27): Error: assertion violation

 Execution trace:

     (0,0): anon0

+    (0,0): anon3_Then

+    (0,0): anon2

 TypeParameters.dfy(130,28): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    (0,0): anon5_Then

+    (0,0): anon14_Then

+    TypeParameters.dfy(130,32): anon15_Else

+    (0,0): anon5

 TypeParameters.dfy(132,33): Error: assertion violation

 Execution trace:

     (0,0): anon0

-    (0,0): anon6_Then

+    (0,0): anon17_Then

+    TypeParameters.dfy(132,37): anon18_Else

+    (0,0): anon11

 

-Dafny program verifier finished with 27 verified, 4 errors

+Dafny program verifier finished with 32 verified, 4 errors

 

 -------------------- Datatypes.dfy --------------------

+Datatypes.dfy(82,20): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon20_Else

+    (0,0): anon21_Then

+    (0,0): anon4

+    (0,0): anon22_Else

+    (0,0): anon23_Then

+    (0,0): anon24_Else

+    (0,0): anon25_Then

+

+Dafny program verifier finished with 11 verified, 1 error

+

+-------------------- TypeAntecedents.dfy --------------------

+TypeAntecedents.dfy(34,13): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+TypeAntecedents.dfy(60,1): Error BP5003: A postcondition might not hold on this return path.

+TypeAntecedents.dfy(59,15): Related location: This is the postcondition that might not hold.

+Execution trace:

+    (0,0): anon0

+    (0,0): anon15_Then

+    (0,0): anon6

+    (0,0): anon18_Then

+    (0,0): anon8

+    (0,0): anon19_Then

+    (0,0): anon10

+    (0,0): anon20_Then

+    (0,0): anon21_Then

+    (0,0): anon14

+TypeAntecedents.dfy(68,16): Error: assertion violation

+Execution trace:

+    (0,0): anon0

+    (0,0): anon15_Else

+    (0,0): anon16_Then

+    (0,0): anon17_Else

 

-Dafny program verifier finished with 10 verified, 0 errors

+Dafny program verifier finished with 12 verified, 3 errors

 

 -------------------- SplitExpr.dfy --------------------

 

diff --git a/Test/dafny0/DTypes.dfy b/Test/dafny0/DTypes.dfy
index d925587b..f92e93e6 100644
--- a/Test/dafny0/DTypes.dfy
+++ b/Test/dafny0/DTypes.dfy
@@ -25,8 +25,7 @@ class C {
   method A1(a: CP<int,C>)

   {

     var x: object := a;

-    assert (forall b: CP<int,Stack> :: x == b ==> b == null);  // error (we don't add a type antecedent to

-                                                               // quantifiers; is that what we want?)

+    assert (forall b: CP<int,Stack> :: x == b ==> b == null);  // follows from type antecedents

   }

 

   var a2x: set<CP<C,Node>>;

diff --git a/Test/dafny0/Datatypes.dfy b/Test/dafny0/Datatypes.dfy
index 2b3168b2..a7ac03d9 100644
--- a/Test/dafny0/Datatypes.dfy
+++ b/Test/dafny0/Datatypes.dfy
@@ -63,3 +63,33 @@ class AnotherNode {
     r.next := n;

   }

 }

+

+method TestAllocatednessAxioms(a: List<Node>, b: List<Node>, c: List<AnotherNode>)

+{

+  var n := new Node;

+  var p := n;

+  match a {

+    case Nil =>

+    case Cons(x, tail) => assert x != n; p := x;

+  }

+  match b {

+    case Nil =>

+    case Cons(x, tail) =>

+      match tail {

+        case Nil =>

+        case Cons(y, more) =>

+          assert y != n;

+          assert y != p;  // error: if p is car(a), then it and y may very well be equal

+      }

+  }

+  match c {

+    case Nil =>

+    case Cons(x, tail) =>

+      match tail {

+        case Nil =>

+        case Cons(y, more) =>

+          var o: object := y;

+          assert p != null ==> p != o;  // follows from well-typedness

+      }

+  }

+}

diff --git a/Test/dafny0/Definedness.dfy b/Test/dafny0/Definedness.dfy
index d4a39179..255b38e3 100644
--- a/Test/dafny0/Definedness.dfy
+++ b/Test/dafny0/Definedness.dfy
@@ -75,26 +75,26 @@ class StatementTwoShoes {
     modifies this, p;

   {

     p.x := a;  // error: receiver may be null

-    F(a).x := a;  // error: LHS may not be well defined

-    x := F(a-10).x;  // error: RHS may not be well defined

+    F(a).x := a;  // error: LHS may not be well defined (fn precondition)

+    x := F(a-10).x;  // error: RHS may not be well defined (fn precondition)

   }

 

   method N(a: int, b: int)

   {

-    assert 5 / a == 5 / a;  // error: expression may not be well defined

-    assume 20 / b == 5;  // error: expression may not be well defined

+    assert 5 / a == 5 / a;  // error: expression may not be well defined (div by zero)

+    assume 20 / b == 5;  // error: expression may not be well defined (div by zero)

   }

 

   method O(a: int) returns (b: int)

   {

-    if (20 / a == 5) {  // error: expression may not be well defined

+    if (20 / a == 5) {  // error: expression may not be well defined (div by zero)

       b := a;

     }

   }

 

   method P(a: int)

   {

-    while (20 / a == 5) {  // error: expression may not be well defined

+    while (20 / a == 5) {  // error: expression may not be well defined (div by zero)

       break;

     }

   }

@@ -103,13 +103,13 @@ class StatementTwoShoes {
   {

     var i := 1;

     while (i < a)

-      decreases F(i), F(a), a - i;  // error: component 1 may not be well defined

+      decreases F(i), F(a), a - i;  // error: component 1 may not be well defined (fn precond)

     {

       i := i + 1;

     }

     i := 1;

     while (i < a)

-      decreases F(b), a - i;  // error: component 0 may not be well defined

+      decreases F(b), a - i;  // error: component 0 may not be well defined (fn precond)

     {

       i := i + 1;

     }

@@ -119,7 +119,7 @@ class StatementTwoShoes {
   {

     var i := 0;

     while (i < 100)  // The following produces 3 complaints instead of 1, because loop invariants are not subject to subsumption

-      invariant F(a) != null;  // error: expression may not be well defined, and error: loop invariant may not hold

+      invariant F(a) != null;  // error: expression may not be well defined (fn precond), and error: loop invariant may not hold

       decreases F(a), 100 - i;  // error: component 0 not well defined

     {

       i := i + 1;

@@ -129,7 +129,7 @@ class StatementTwoShoes {
   method S(a: int)

   {

     var j := 0;

-    while (20 / a == 5 && j < 100)  // error: guard may not be well defined

+    while (20 / a == 5 && j < 100)  // error: guard may not be well defined (div by zero)

       invariant j <= 100;

       decreases F(101 - j), 100 - j;

     {

@@ -148,7 +148,7 @@ class StatementTwoShoes {
       j := j + 1;

     }

     j := 0;

-    while (20 / k == 5 && j < 100)  // error: guard may not be well defined

+    while (20 / k == 5 && j < 100)  // error: guard may not be well defined (div by zero)

       decreases 100 - j;

     {

       havoc k;

@@ -167,7 +167,7 @@ class StatementTwoShoes {
     }

     i := 0;

     while (i < 100)

-      invariant F(if i==77 then -3 else i) == this;  // error: expression may not be well defined

+      invariant F(if i==77 then -3 else i) == this;  // error: expression may not be well defined (fn precond)

     {

       i := i + 1;

       if (i == 77) { i := i + 1; }

@@ -188,7 +188,7 @@ class StatementTwoShoes {
       use G(5 / m.x);  // fine, because there are no welldefinedness checks on use statements

       m.x := m.x + 1;

     }

-    foreach (m in s + {F(a)})  // error: collection expression may not be well defined

+    foreach (m in s + {F(a)})  // error: collection expression may not be well defined (fn precondition)

     {

       m.x := 5;  // error: possible modifies clause violation

     }

@@ -207,7 +207,7 @@ class StatementTwoShoes {
     var i := 0;

     while (i < 100)

       // The following line produces two complaints, thanks to the w-encoding of the loop's invariant definedness checking

-      invariant 5 / x != 5 / x;  // error: not well-defined, and error: loop invariant does not hold initially

+      invariant 5 / x != 5 / x;  // error: not well-defined (div by zero), and error: loop invariant does not hold initially

     {

       i := i + 1;

     }

diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index 87bfd35f..2eca82fd 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -79,8 +79,8 @@ class Modifies {
   {

     x := x + 1;

     while (p != null && p.x < 75)

-      decreases 75 - p.x;  // error: not defined at top of each iteration (there's good reason to

-    {                      // insist on this; for example, the decrement check could not be performed

+      decreases 75 - p.x;  // error: not defined (null deref) at top of each iteration (there's good reason

+    {                      // to insist on this; for example, the decrement check could not be performed

       p.x := p.x + 1;      // at the end of the loop body if p were set to null in the loop body)

     }

   }

@@ -182,3 +182,53 @@ class Modifies {
     }

   }

 }

+

+// ------------------ allocated --------------------------------------------------

+

+class AllocatedTests {

+  method M(r: AllocatedTests, k: Node, S: set<Node>, d: Lindgren)

+  {

+    assert allocated(r);

+    

+    var n := new Node;

+    var t := S + {n};

+    assert allocated(t);

+

+    assert allocated(d);

+    if (*) {

+      assert old(allocated(n));  // error: n was not allocated in the initial state

+    } else {

+      assert !old(allocated(n));  // correct

+    }

+

+    var U := {k,n};

+    if (*) {

+      assert old(allocated(U));  // error: n was not allocated initially

+    } else {

+      assert !old(allocated(U));  // correct (note, the assertion does NOT say: everything was unallocated in the initial state)

+    }

+

+    assert allocated(6);

+    assert allocated(6);

+    assert allocated(null);

+    assert allocated(#Lindgren.HerrNilsson);

+

+    match (d) {

+      case Pippi(n) => assert allocated(n);

+      case Longstocking(q, dd) => assert allocated(q); assert allocated(dd);

+      case HerrNilsson => assert old(allocated(d));

+    }

+    var ls := #Lindgren.Longstocking([], d);

+    assert allocated(ls);

+    assert old(allocated(ls));

+

+    assert old(allocated(#Lindgren.Longstocking([r], d)));

+    assert old(allocated(#Lindgren.Longstocking([n], d)));  // error, because n was not allocated initially

+  }

+}

+

+datatype Lindgren {

+  Pippi(Node);

+  Longstocking(seq<object>, Lindgren);

+  HerrNilsson;

+}

diff --git a/Test/dafny0/Termination.dfy b/Test/dafny0/Termination.dfy
index a5aca6ff..779c9892 100644
--- a/Test/dafny0/Termination.dfy
+++ b/Test/dafny0/Termination.dfy
@@ -264,3 +264,51 @@ function Zipper2<T>(a: List<T>, b: List<T>): List<T>
   case Nil => b

   case Cons(x, c) => #List.Cons(x, Zipper2(b, c))

 }

+

+// -------------------------- test translation of while (*) -----------------

+

+method WhileStar0(n: int)

+  requires 2 <= n;

+{

+  var m := n;

+  var k := 0;

+  while (*)

+    invariant 0 <= k && 0 <= m;

+    decreases *;

+  {

+    k := k + m;

+    m := m + k;

+  }

+  assert 0 <= k;

+}

+

+method WhileStar1()

+{

+  var k := 0;

+  while (*)  // error: failure to prove termination

+  {

+    k := k + 1;

+    if (k == 17) { break; }

+  }

+}

+

+method WhileStar2()

+{

+  var k := 0;

+  while (*)

+    invariant k < 17;

+    decreases 17 - k;

+  {

+    k := k + 1;

+    if (k == 17) { break; }

+  }

+}

+

+// -----------------

+

+function ReachBack(n: int): bool

+  requires 0 <= n;

+  ensures ReachBack(n);

+{

+  (forall m :: 0 <= m && m < n ==> ReachBack(m))

+}

diff --git a/Test/dafny0/TypeAntecedents.dfy b/Test/dafny0/TypeAntecedents.dfy
new file mode 100644
index 00000000..6fe86493
--- /dev/null
+++ b/Test/dafny0/TypeAntecedents.dfy
@@ -0,0 +1,104 @@
+// -------- This is an example of what was once logically (although not trigger-ly) unsound ---

+

+datatype Wrapper<T> {

+  Wrap(T);

+}

+datatype Unit { It; }

+datatype Color { Yellow; Blue; }

+

+function F(a: Wrapper<Unit>): bool

+  ensures a == #Wrapper.Wrap(#Unit.It);

+{

+  match a

+  case Wrap(u) => G(u)

+}

+

+function G(u: Unit): bool

+  ensures u == #Unit.It;

+{

+  match u

+  case It => true

+}

+

+method BadLemma(c0: Color, c1: Color)

+  ensures c0 == c1;

+{

+  var w0 := #Wrapper.Wrap(c0);

+  var w1 := #Wrapper.Wrap(c1);

+

+  // Manually, add the following assertions in Boogie.  (These would

+  // be ill-typed in Dafny.)

+  //     assert _default.F($Heap, this, w0#6);

+  //     assert _default.F($Heap, this, w1#7);

+

+  assert w0 == w1;  // this would be bad news (it should be reported as an error)

+}

+

+method Main() {

+  call BadLemma(#Color.Yellow, #Color.Blue);

+  assert false;  // this shows how things can really go wrong if BadLemma verified successfully

+}

+

+// ---------------

+

+class MyClass {

+  var x: int;

+  // The function axiom has "DType(this) == class.MyClass" in its antecedent.  Hence, it

+  // is possible to prove the various asserts below only if the receiver is known by the

+  // verifier to be of type MyClass.

+  function H(): int { 5 }

+}

+

+datatype List {

+  Nil;

+  Cons(MyClass, List);

+}

+

+method M(list: List, S: set<MyClass>) returns (ret: int)

+  modifies S;

+  ensures ret == 7;

+{  // error: postcondition violation (this postcondition tests that control does flow to the end)

+  match (list) {

+    case Nil =>

+    case Cons(r,tail) =>

+      if (r != null) {

+        ghost var h := r.H();

+        assert h == 5;

+      } else {

+        assert false;  // error

+      }

+  }

+  call k := N();

+  assert k.H() == 5;

+  ghost var l := NF();

+  assert l != null ==> l.H() == 5;

+

+  foreach (s in S) {

+    assert s == null || s.H() == 5;

+    s.x := 0;

+  }

+

+  assert (forall t: MyClass :: t == null || t.H() == 5);

+  // note, the definedness problem in the next line sits inside an unreachable branch

+  assert (forall t: MyClass :: t != null ==> (if t.H() == 5 then true else 10 / 0 == 3));

+

+  assert TakesADatatype(#List.Nil) == 12;

+  assert TakesADatatype(#List.Cons(null, #List.Nil)) == 12;

+  assert AlsoTakesADatatype(#GenData.Pair(false, true)) == 17;

+}

+

+method N() returns (k: MyClass)

+  ensures k != null;

+{

+  k := new MyClass;

+}

+

+function NF(): MyClass;

+

+function TakesADatatype(a: List): int { 12 }

+

+datatype GenData<T> {

+  Pair(T, T);

+}

+

+function AlsoTakesADatatype<U>(p: GenData<U>): int { 17 }

diff --git a/Test/dafny0/TypeParameters.dfy b/Test/dafny0/TypeParameters.dfy
index 61a0019b..7aaf5ad3 100644
--- a/Test/dafny0/TypeParameters.dfy
+++ b/Test/dafny0/TypeParameters.dfy
@@ -132,3 +132,29 @@ method IsRogerCool(n: int)
     assert RogerThat(2 < 3 && n < n && n < n+1);  // same here; cool, huh?

   }

 }

+

+// ----------------------

+

+class TyKn_C<T> {

+  var x: T;

+  function G(): T;

+  method M() returns (t: T);

+}

+

+class TyKn_K {

+  function F(): int { 176 }

+}

+

+method TyKn_Main(k0: TyKn_K) {

+  var c := new TyKn_C<TyKn_K>;

+  var k1: TyKn_K;

+

+  assert k0 != null ==> k0.F() == 176;

+  assert k1 != null ==> k1.F() == 176;

+

+  assert c.x != null ==> c.x.F() == 176;  // the Dafny encoding needs the canCall mechanism to verify this

+  assert c.G() != null ==> c.G().F() == 176;  // ditto

+  call k2 := c.M();

+  assert k2 != null ==> k2.F() == 176;  // the canCall mechanism does the trick here, but so does the encoding

+                                        // via k2's where clause

+}

diff --git a/Test/dafny0/runtest.bat b/Test/dafny0/runtest.bat
index c92ae0a2..3e9507ef 100644
--- a/Test/dafny0/runtest.bat
+++ b/Test/dafny0/runtest.bat
@@ -15,7 +15,8 @@ for %%f in (TypeTests.dfy SmallTests.dfy Definedness.dfy FunctionSpecifications.
             Array.dfy MultiDimArray.dfy

             Modules0.dfy Modules1.dfy BadFunction.dfy

             Termination.dfy Use.dfy DTypes.dfy

-            TypeParameters.dfy Datatypes.dfy SplitExpr.dfy Refinement.dfy RefinementErrors.dfy) do (

+            TypeParameters.dfy Datatypes.dfy TypeAntecedents.dfy SplitExpr.dfy

+            Refinement.dfy RefinementErrors.dfy) do (

   echo.

   echo -------------------- %%f --------------------

   %DAFNY_EXE% /compile:0 %* %%f

diff --git a/Test/dafny1/SchorrWaite.dfy b/Test/dafny1/SchorrWaite.dfy
index 52db9dca..0d69b1b8 100644
--- a/Test/dafny1/SchorrWaite.dfy
+++ b/Test/dafny1/SchorrWaite.dfy
@@ -211,7 +211,9 @@ class Main {
                   (forall j :: 0 <= j && j < |n.children| ==>

                     j == n.childrenVisited || n.children[j] == old(n.children[j])));

       // every marked node is reachable:

+      invariant old(allocated(path));  // needed to show 'path' worthy as argument to old(Reachable(...))

       invariant old(ReachableVia(root, path, t, S));

+      invariant (forall n, pth :: n in S && n.marked && pth == n.pathFromRoot ==> old(allocated(pth)));

       invariant (forall n, pth :: n in S && n.marked && pth == n.pathFromRoot ==>

                   old(ReachableVia(root, pth, n, S)));

       invariant (forall n :: n in S && n.marked ==> old(Reachable(root, n, S)));

diff --git a/Util/Emacs/dafny-mode.el b/Util/Emacs/dafny-mode.el
index 82490ae7..cc3d6fb2 100644
--- a/Util/Emacs/dafny-mode.el
+++ b/Util/Emacs/dafny-mode.el
@@ -37,7 +37,7 @@
         )) . font-lock-builtin-face)

    `(,(dafny-regexp-opt '(

         "assert" "assume" "break" "call" "then" "else" "havoc" "if" "label" "return" "while" "print"

-        "old" "forall" "exists" "new" "foreach" "in" "this" "fresh" "use"

+        "old" "forall" "exists" "new" "foreach" "in" "this" "fresh" "allocated" "use"

         "match" "case" "false" "true" "null")) . font-lock-keyword-face)

    `(,(dafny-regexp-opt '("array" "array2" "array3" "bool" "int" "object" "set" "seq")) . font-lock-type-face)

    )

diff --git a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
index 48841c43..26d4f45a 100644
--- a/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
+++ b/Util/VS2010/Dafny/DafnyLanguageService/Grammar.cs
@@ -27,7 +27,7 @@ namespace Demo
           "in", "forall", "exists",

           "seq", "set", "array", "array2", "array3",

           "match", "case",

-          "fresh", "old"

+          "fresh", "allocated", "old"

           );

 

         StringLiteral s = new StringLiteral("String", "'", StringFlags.AllowsDoubledQuote);

@@ -335,6 +335,7 @@ namespace Demo
           | "match"

           | "case"

           | "fresh"

+          | "allocated"

           | "old"

           | ident

           | "}"

diff --git a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
index a9254621..a4d67f0b 100644
--- a/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
+++ b/Util/VS2010/DafnyExtension/DafnyExtension/TokenTagger.cs
@@ -233,6 +233,7 @@ namespace DafnyLanguage
             } else {

               switch (s) {

                 #region keywords

+                case "allocated":

                 case "array":

                 case "assert":

                 case "assume":

diff --git a/Util/latex/dafny.sty b/Util/latex/dafny.sty
index e82ed0dc..11af30d4 100644
--- a/Util/latex/dafny.sty
+++ b/Util/latex/dafny.sty
@@ -11,7 +11,7 @@
       method,returns,module,imports,in,

       requires,modifies,ensures,reads,decreases,free,

       % expressions

-      match,case,false,true,null,old,fresh,this,

+      match,case,false,true,null,old,fresh,allocated,this,

       % statements

       assert,assume,print,new,havoc,call,if,then,else,while,invariant,break,label,return,foreach,

       },

diff --git a/Util/vim/syntax/dafny.vim b/Util/vim/syntax/dafny.vim
index df2666c3..5c492a31 100644
--- a/Util/vim/syntax/dafny.vim
+++ b/Util/vim/syntax/dafny.vim
@@ -13,7 +13,7 @@ syntax keyword dafnyStatement havoc assume assert return call new print break la
 syntax keyword dafnyKeyword var ghost returns null static this refines replaces by
 syntax keyword dafnyType int bool seq set object array array2 array3
 syntax keyword dafnyLogic requires ensures modifies reads decreases invariant 
-syntax keyword dafnyOperator forall exists old fresh
+syntax keyword dafnyOperator forall exists old fresh allocated
 syntax keyword dafnyBoolean true false
   
 syntax region dafnyString start=/"/ skip=/\\"/ end=/"/