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(*)

8 files changed, 842 insertions, 530 deletions

diff --git a/Source/Dafny/Compiler.cs b/Source/Dafny/Compiler.cs
index a00ca0b0..dc7caac7 100644
--- a/Source/Dafny/Compiler.cs
+++ b/Source/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/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index ef7164bc..c4955a6a 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/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/Source/Dafny/DafnyAst.cs b/Source/Dafny/DafnyAst.cs
index 9eec1e39..1ae19313 100644
--- a/Source/Dafny/DafnyAst.cs
+++ b/Source/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/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 1837ea9e..290609fc 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/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/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index dd4c7be5..0b93a1dc 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/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/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs
index 6c062820..080930ea 100644
--- a/Source/Dafny/Resolver.cs
+++ b/Source/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/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs
index de87c6ad..b7e7f57b 100644
--- a/Source/Dafny/Scanner.cs
+++ b/Source/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/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index 0a96a197..181ec9ec 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/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);