Merge

3 files changed, 361 insertions, 281 deletions

diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 2eaaca7f..7019a22b 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -191,6 +191,7 @@ ClassDecl<ModuleDecl/*!*/ module, out ClassDecl/*!*/ c>
      List<MemberDecl/*!*/> members = new List<MemberDecl/*!*/>();

      IToken bodyStart;

   .)

+  SYNC

   "class"

   { Attribute<ref attrs> }

   Ident<out id>

@@ -234,6 +235,7 @@ DatatypeDecl<ModuleDecl/*!*/ module, out DatatypeDecl/*!*/ dt>
      List<DatatypeCtor/*!*/> ctors = new List<DatatypeCtor/*!*/>();

      IToken bodyStart = Token.NoToken;  // dummy assignment

   .)

+  SYNC

   "datatype"

   { Attribute<ref attrs> }

   Ident<out id>

@@ -241,7 +243,7 @@ DatatypeDecl<ModuleDecl/*!*/ module, out DatatypeDecl/*!*/ dt>
   "="                                      (. bodyStart = t; .)

   DatatypeMemberDecl<ctors>

   { "|" DatatypeMemberDecl<ctors> }

-  ";"

+  SYNC ";"

   (. dt = new DatatypeDecl(id, id.val, module, typeArgs, ctors, attrs);

      dt.BodyStartTok = bodyStart;

      dt.BodyEndTok = t;

@@ -263,6 +265,7 @@ FieldDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.>
      Attributes attrs = null;

      IToken/*!*/ id;  Type/*!*/ ty;

   .)

+  SYNC

   "var"

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

      if (mmod.IsStatic) { SemErr(t, "fields cannot be declared 'static'"); }

@@ -271,7 +274,7 @@ FieldDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.>
   IdentType<out id, out ty>                         (. mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); .)

   { "," IdentType<out id, out ty>                   (. mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); .)

   }

-  ";"

+  SYNC ";"

   .

 CouplingInvDecl<.MemberModifiers mmod, List<MemberDecl/*!*/>/*!*/ mm.>

 = (. Contract.Requires(cce.NonNullElements(mm));

@@ -379,6 +382,7 @@ MethodDecl<MemberModifiers mmod, bool allowConstructor, out Method/*!*/ m>
      IToken bodyStart = Token.NoToken;

      IToken bodyEnd = Token.NoToken;

   .)

+  SYNC

   ( "method"

   | "constructor"                   (. if (allowConstructor) {

                                          isConstructor = true;

@@ -423,16 +427,17 @@ MethodSpec<.List<MaybeFreeExpression/*!*/>/*!*/ req, List<FrameExpression/*!*/>/
 = (. Contract.Requires(cce.NonNullElements(req)); Contract.Requires(cce.NonNullElements(mod)); Contract.Requires(cce.NonNullElements(ens)); Contract.Requires(cce.NonNullElements(decreases));

      Expression/*!*/ e;  FrameExpression/*!*/ fe;  bool isFree = false;

   .)

+  SYNC

   ( "modifies" [ FrameExpression<out fe>                     (. mod.Add(fe); .)

                  { "," FrameExpression<out fe>               (. mod.Add(fe); .)

                  }

-               ] ";"

+               ] SYNC ";"

   | [ "free"                                                 (. isFree = true; .)

     ]

-    ( "requires" Expression<out e> ";"                       (. req.Add(new MaybeFreeExpression(e, isFree)); .)

-    | "ensures" Expression<out e> ";"                        (. ens.Add(new MaybeFreeExpression(e, isFree)); .)

+    ( "requires" Expression<out e> SYNC ";"                       (. req.Add(new MaybeFreeExpression(e, isFree)); .)

+    | "ensures" Expression<out e> SYNC ";"                        (. ens.Add(new MaybeFreeExpression(e, isFree)); .)

     )

-  | "decreases" DecreasesList<decreases, false> ";"

+  | "decreases" DecreasesList<decreases, false> SYNC ";"

   )

   .

 Formals<.bool incoming, bool allowGhostKeyword, List<Formal/*!*/>/*!*/ formals.>

@@ -555,13 +560,15 @@ FunctionDecl<MemberModifiers mmod, out Function/*!*/ f>
 FunctionSpec<.List<Expression/*!*/>/*!*/ reqs, List<FrameExpression/*!*/>/*!*/ reads, List<Expression/*!*/>/*!*/ ens, List<Expression/*!*/>/*!*/ decreases.>

 = (. Contract.Requires(cce.NonNullElements(reqs)); Contract.Requires(cce.NonNullElements(reads)); Contract.Requires(cce.NonNullElements(decreases));

      Expression/*!*/ e;  FrameExpression/*!*/ fe; .)

-  ( "requires" Expression<out e> ";"      (. reqs.Add(e); .)

+  (

+    SYNC

+    "requires" Expression<out e> SYNC ";"      (. reqs.Add(e); .)

   | "reads" [ PossiblyWildFrameExpression<out fe>              (. reads.Add(fe); .)

               { "," PossiblyWildFrameExpression<out fe>        (. reads.Add(fe); .)

               }

-            ] ";"

-  | "ensures" Expression<out e> ";"      (. ens.Add(e); .)

-  | "decreases" DecreasesList<decreases, false> ";"

+            ] SYNC ";"

+  | "ensures" Expression<out e> SYNC ";"      (. ens.Add(e); .)

+  | "decreases" DecreasesList<decreases, false> SYNC ";"

   )

   .

 PossiblyWildExpression<out Expression/*!*/ e>

@@ -622,6 +629,7 @@ OneStmt<out Statement/*!*/ s>
      int breakCount;

   .)

   /* This list does not contain BlockStmt, see comment above in Stmt production. */

+  SYNC

   ( BlockStmt<out s, out bodyStart, out bodyEnd>

   | AssertStmt<out s>

   | AssumeStmt<out s>

@@ -640,6 +648,7 @@ OneStmt<out Statement/*!*/ s>
     | { "break"                        (. breakCount++; .)

       }

     )

+    SYNC

     ";"                                (. s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount); .)

   | ReturnStmt<out s>

   )

@@ -814,25 +823,29 @@ WhileStmt<out Statement/*!*/ stmt>
   )

   .

 LoopSpec<.out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!*/> decreases, out List<FrameExpression/*!*/> mod.>

-= (. bool isFree;  Expression/*!*/ e; FrameExpression/*!*/ fe;

+= (. FrameExpression/*!*/ fe;

      invariants = new List<MaybeFreeExpression/*!*/>();

+     MaybeFreeExpression invariant = null;

      decreases = new List<Expression/*!*/>();

      mod = null;

   .)

-  {                         (. isFree = false; .)

-    [ "free"                (. isFree = true; .)

-    ]

-    "invariant"

-    Expression<out e>       (. invariants.Add(new MaybeFreeExpression(e, isFree)); .)

-    ";"

-  | "decreases" DecreasesList<decreases, true> ";"

-  | "modifies" (. mod = mod ?? new List<FrameExpression>(); .)

+  {

+    Invariant<out invariant> SYNC ";"   (. invariants.Add(invariant); .)

+  | SYNC "decreases" DecreasesList<decreases, true> SYNC ";"

+  | SYNC "modifies" (. mod = mod ?? new List<FrameExpression>(); .)

                [ FrameExpression<out fe>                     (. mod.Add(fe); .)

                  { "," FrameExpression<out fe>               (. mod.Add(fe); .)

                  }

-               ] ";"

+               ] SYNC ";"

   }

   .

+Invariant<out MaybeFreeExpression/*!*/ invariant>

+= (. bool isFree = false; Expression/*!*/ e; invariant = null; .)

+    SYNC

+    ["free"                                 (. isFree = true; .)

+    ]

+    "invariant" Expression<out e>           (. invariant = new MaybeFreeExpression(e, isFree); .)

+  .

 DecreasesList<.List<Expression/*!*/> decreases, bool allowWildcard.>

 = (. Expression/*!*/ e; .)

   PossiblyWildExpression<out e>          (. if (!allowWildcard && e is WildcardExpr) {

@@ -1310,8 +1323,8 @@ Suffix<ref Expression/*!*/ e>
           }

         )

       | ".."                                   (. anyDots = true; .)

-	    [ Expression<out ee>                   (. e1 = ee; .)

-	    ]

+        [ Expression<out ee>                   (. e1 = ee; .)

+        ]

       )

       (. if (multipleIndices != null) {

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

diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 583fcc61..f723ad2c 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -23,7 +23,7 @@ public class Parser {
 	const bool T = true;

 	const bool x = false;

 	const int minErrDist = 2;

-	

+

 	public Scanner/*!*/ scanner;

 	public Errors/*!*/  errors;

 

@@ -134,10 +134,10 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		if (errDist >= minErrDist) errors.SemErr(t, msg);

 		errDist = 0;

 	}

-	

-    public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {

-      Contract.Requires(tok != null);

-      Contract.Requires(msg != null);

+

+	public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {

+	  Contract.Requires(tok != null);

+	  Contract.Requires(msg != null);

 	  errors.SemErr(tok, msg);

 	}

 

@@ -150,15 +150,15 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			la = t;

 		}

 	}

-	

+

 	void Expect (int n) {

 		if (la.kind==n) Get(); else { SynErr(n); }

 	}

-	

+

 	bool StartOf (int s) {

 		return set[s, la.kind];

 	}

-	

+

 	void ExpectWeak (int n, int follow) {

 		if (la.kind == n) Get();

 		else {

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

 	}

 

-	

+

 	void Dafny() {

 		ClassDecl/*!*/ c; DatatypeDecl/*!*/ dt;

 		Attributes attrs;  IToken/*!*/ id;  List<string/*!*/> theImports;

@@ -191,13 +191,13 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		// to support multiple files, create a default module only if theModules doesn't already contain one

 		DefaultModuleDecl defaultModule = null;

 		foreach (ModuleDecl mdecl in theModules) {

-		  defaultModule = mdecl as DefaultModuleDecl;

-		  if (defaultModule != null) { break; }

+		 defaultModule = mdecl as DefaultModuleDecl;

+		 if (defaultModule != null) { break; }

 		}

 		bool defaultModuleCreatedHere = false;

 		if (defaultModule == null) {

-		  defaultModuleCreatedHere = true;

-		  defaultModule = new DefaultModuleDecl();

+		 defaultModuleCreatedHere = true;

+		 defaultModule = new DefaultModuleDecl();

 		}

 		

 		while (StartOf(1)) {

@@ -241,14 +241,14 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		 defaultModule.TopLevelDecls.Add(new DefaultClassDecl(defaultModule, membersDefaultClass));

 		 theModules.Add(defaultModule);

 		} else {

-		  // find the default class in the default module, then append membersDefaultClass to its member list

-		  foreach (TopLevelDecl topleveldecl in defaultModule.TopLevelDecls) {

-		    DefaultClassDecl defaultClass = topleveldecl as DefaultClassDecl;

-		    if (defaultClass != null) {

-		      defaultClass.Members.AddRange(membersDefaultClass);

-		      break;

-		    }

-		  }

+		 // find the default class in the default module, then append membersDefaultClass to its member list

+		 foreach (TopLevelDecl topleveldecl in defaultModule.TopLevelDecls) {

+		   DefaultClassDecl defaultClass = topleveldecl as DefaultClassDecl;

+		   if (defaultClass != null) {

+		     defaultClass.Members.AddRange(membersDefaultClass);

+		     break;

+		   }

+		 }

 		}

 		

 		Expect(0);

@@ -288,6 +288,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		List<MemberDecl/*!*/> members = new List<MemberDecl/*!*/>();

 		IToken bodyStart;

 		

+		while (!(la.kind == 0 || la.kind == 9)) {SynErr(105); Get();}

 		Expect(9);

 		while (la.kind == 7) {

 			Attribute(ref attrs);

@@ -310,7 +311,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		if (optionalId == null)

 		 c = new ClassDecl(id, id.val, module, typeArgs, members, attrs);

 		else

-		  c = new ClassRefinementDecl(id, id.val, module, typeArgs, members, attrs, optionalId);

+		 c = new ClassRefinementDecl(id, id.val, module, typeArgs, members, attrs, optionalId);

 		c.BodyStartTok = bodyStart;

 		c.BodyEndTok = t;

 		

@@ -325,6 +326,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		List<DatatypeCtor/*!*/> ctors = new List<DatatypeCtor/*!*/>();

 		IToken bodyStart = Token.NoToken;  // dummy assignment

 		

+		while (!(la.kind == 0 || la.kind == 14)) {SynErr(106); Get();}

 		Expect(14);

 		while (la.kind == 7) {

 			Attribute(ref attrs);

@@ -340,6 +342,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			Get();

 			DatatypeMemberDecl(ctors);

 		}

+		while (!(la.kind == 0 || la.kind == 17)) {SynErr(107); Get();}

 		Expect(17);

 		dt = new DatatypeDecl(id, id.val, module, typeArgs, ctors, attrs);

 		dt.BodyStartTok = bodyStart;

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

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

 			CouplingInvDecl(mmod, mm);

-		} else SynErr(105);

+		} else SynErr(108);

 	}

 

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

@@ -397,6 +400,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		Attributes attrs = null;

 		IToken/*!*/ id;  Type/*!*/ ty;

 		

+		while (!(la.kind == 0 || la.kind == 18)) {SynErr(109); Get();}

 		Expect(18);

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

 		if (mmod.IsStatic) { SemErr(t, "fields cannot be declared 'static'"); }

@@ -411,6 +415,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			IdentType(out id, out ty);

 			mm.Add(new Field(id, id.val, mmod.IsGhost, ty, attrs)); 

 		}

+		while (!(la.kind == 0 || la.kind == 17)) {SynErr(110); Get();}

 		Expect(17);

 	}

 

@@ -477,6 +482,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		IToken bodyStart = Token.NoToken;

 		IToken bodyEnd = Token.NoToken;

 		

+		while (!(StartOf(4))) {SynErr(111); Get();}

 		if (la.kind == 25) {

 			Get();

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

@@ -484,21 +490,21 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			if (allowConstructor) {

 			 isConstructor = true;

 			} else {

-			  SemErr(t, "constructors are only allowed in classes");

+			 SemErr(t, "constructors are only allowed in classes");

 			}

 			

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

 			Get();

 			isRefinement = true; 

-		} else SynErr(106);

+		} else SynErr(112);

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

 		if (isConstructor) {

-		  if (mmod.IsGhost) {

-		    SemErr(t, "constructors cannot be declared 'ghost'");

-		  }

-		  if (mmod.IsStatic) {

-		    SemErr(t, "constructors cannot be declared 'static'");

-		  }

+		 if (mmod.IsGhost) {

+		   SemErr(t, "constructors cannot be declared 'ghost'");

+		 }

+		 if (mmod.IsStatic) {

+		   SemErr(t, "constructors cannot be declared 'static'");

+		 }

 		}

 		

 		while (la.kind == 7) {

@@ -514,7 +520,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			if (isConstructor) { SemErr(t, "constructors cannot have out-parameters"); } 

 			Formals(false, !mmod.IsGhost, outs);

 		}

-		while (StartOf(4)) {

+		while (StartOf(5)) {

 			MethodSpec(req, mod, ens, dec);

 		}

 		if (la.kind == 7) {

@@ -524,9 +530,9 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		if (isRefinement)

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

 		else if (isConstructor)

-		  m = new Constructor(id, id.val, typeArgs, ins, req, mod, ens, dec, body, attrs);

+		 m = new Constructor(id, id.val, typeArgs, ins, req, mod, ens, dec, body, attrs);

 		else

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

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

 		m.BodyStartTok = bodyStart;

 		m.BodyEndTok = bodyEnd;

 		

@@ -579,7 +585,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 	void FormalsOptionalIds(List<Formal/*!*/>/*!*/ formals) {

 		Contract.Requires(cce.NonNullElements(formals)); IToken/*!*/ id;  Type/*!*/ ty;  string/*!*/ name;  bool isGhost; 

 		Expect(33);

-		if (StartOf(5)) {

+		if (StartOf(6)) {

 			TypeIdentOptional(out id, out name, out ty, out isGhost);

 			formals.Add(new Formal(id, name, ty, true, isGhost)); 

 			while (la.kind == 19) {

@@ -656,9 +662,9 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			Get();

 			UserDefinedType udt = ty as UserDefinedType;

 			if (udt != null && udt.TypeArgs.Count == 0) {

-			  name = udt.Name;

+			 name = udt.Name;

 			} else {

-			  SemErr(id, "invalid formal-parameter name in datatype constructor");

+			 SemErr(id, "invalid formal-parameter name in datatype constructor");

 			}

 			

 			Type(out ty);

@@ -666,7 +672,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 		if (name != null) {

 		 identName = name;

 		} else {

-		  identName = "#" + anonymousIds++;

+		 identName = "#" + anonymousIds++;

 		}

 		

 	}

@@ -728,7 +734,7 @@ public static int Parse (string/*!*/ s, string/*!*/ filename, List<ModuleDecl/*!
 			ReferenceType(out tok, out ty);

 			break;

 		}

-		default: SynErr(107); break;

+		default: SynErr(113); break;

 		}

 	}

 

@@ -752,9 +758,10 @@ List<Expression/*!*/>/*!*/ decreases) {
 		Contract.Requires(cce.NonNullElements(req)); Contract.Requires(cce.NonNullElements(mod)); Contract.Requires(cce.NonNullElements(ens)); Contract.Requires(cce.NonNullElements(decreases));

 		Expression/*!*/ e;  FrameExpression/*!*/ fe;  bool isFree = false;

 		

+		while (!(StartOf(7))) {SynErr(114); Get();}

 		if (la.kind == 28) {

 			Get();

-			if (StartOf(6)) {

+			if (StartOf(8)) {

 				FrameExpression(out fe);

 				mod.Add(fe); 

 				while (la.kind == 19) {

@@ -763,6 +770,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 					mod.Add(fe); 

 				}

 			}

+			while (!(la.kind == 0 || la.kind == 17)) {SynErr(115); Get();}

 			Expect(17);

 		} else if (la.kind == 29 || la.kind == 30 || la.kind == 31) {

 			if (la.kind == 29) {

@@ -772,19 +780,22 @@ List<Expression/*!*/>/*!*/ decreases) {
 			if (la.kind == 30) {

 				Get();

 				Expression(out e);

+				while (!(la.kind == 0 || la.kind == 17)) {SynErr(116); Get();}

 				Expect(17);

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

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

 				Get();

 				Expression(out e);

+				while (!(la.kind == 0 || la.kind == 17)) {SynErr(117); Get();}

 				Expect(17);

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

-			} else SynErr(108);

+			} else SynErr(118);

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

 			Get();

 			DecreasesList(decreases, false);

+			while (!(la.kind == 0 || la.kind == 17)) {SynErr(119); Get();}

 			Expect(17);

-		} else SynErr(109);

+		} else SynErr(120);

 	}

 

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

@@ -793,7 +804,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		

 		Expect(7);

 		bodyStart = t; 

-		while (StartOf(7)) {

+		while (StartOf(9)) {

 			Stmt(body);

 		}

 		Expect(8);

@@ -818,7 +829,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		if (!allowWildcard && e is WildcardExpr) {

 		 SemErr(e.tok, "'decreases *' is only allowed on loops");

 		} else {

-		  decreases.Add(e);

+		 decreases.Add(e);

 		}

 		

 		while (la.kind == 19) {

@@ -827,7 +838,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			if (!allowWildcard && e is WildcardExpr) {

 			 SemErr(e.tok, "'decreases *' is only allowed on loops");

 			} else {

-			  decreases.Add(e);

+			 decreases.Add(e);

 			}

 			

 		}

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

 			int dims = 1;

 			if (tok.val.Length != 5) {

-			  dims = int.Parse(tok.val.Substring(5));

+			 dims = int.Parse(tok.val.Substring(5));

 			}

 			ty = theBuiltIns.ArrayType(tok, dims, gt[0], true);

 			

@@ -874,20 +885,22 @@ List<Expression/*!*/>/*!*/ decreases) {
 				GenericInstantiation(gt);

 			}

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

-		} else SynErr(110);

+		} else SynErr(121);

 	}

 

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

 		Contract.Requires(cce.NonNullElements(reqs)); Contract.Requires(cce.NonNullElements(reads)); Contract.Requires(cce.NonNullElements(decreases));

 		Expression/*!*/ e;  FrameExpression/*!*/ fe; 

 		if (la.kind == 30) {

+			while (!(la.kind == 0 || la.kind == 30)) {SynErr(122); Get();}

 			Get();

 			Expression(out e);

+			while (!(la.kind == 0 || la.kind == 17)) {SynErr(123); Get();}

 			Expect(17);

 			reqs.Add(e); 

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

 			Get();

-			if (StartOf(8)) {

+			if (StartOf(10)) {

 				PossiblyWildFrameExpression(out fe);

 				reads.Add(fe); 

 				while (la.kind == 19) {

@@ -896,17 +909,20 @@ List<Expression/*!*/>/*!*/ decreases) {
 					reads.Add(fe); 

 				}

 			}

+			while (!(la.kind == 0 || la.kind == 17)) {SynErr(124); Get();}

 			Expect(17);

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

 			Get();

 			Expression(out e);

+			while (!(la.kind == 0 || la.kind == 17)) {SynErr(125); Get();}

 			Expect(17);

 			ens.Add(e); 

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

 			Get();

 			DecreasesList(decreases, false);

+			while (!(la.kind == 0 || la.kind == 17)) {SynErr(126); Get();}

 			Expect(17);

-		} else SynErr(111);

+		} else SynErr(127);

 	}

 

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

@@ -923,9 +939,9 @@ List<Expression/*!*/>/*!*/ decreases) {
 		if (la.kind == 44) {

 			Get();

 			fe = new FrameExpression(new WildcardExpr(t), null); 

-		} else if (StartOf(6)) {

+		} else if (StartOf(8)) {

 			FrameExpression(out fe);

-		} else SynErr(112);

+		} else SynErr(128);

 	}

 

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

@@ -934,9 +950,9 @@ List<Expression/*!*/>/*!*/ decreases) {
 		if (la.kind == 44) {

 			Get();

 			e = new WildcardExpr(t); 

-		} else if (StartOf(6)) {

+		} else if (StartOf(8)) {

 			Expression(out e);

-		} else SynErr(113);

+		} else SynErr(129);

 	}

 

 	void Stmt(List<Statement/*!*/>/*!*/ ss) {

@@ -952,6 +968,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		IToken bodyStart, bodyEnd;

 		int breakCount;

 		

+		while (!(StartOf(11))) {SynErr(130); Get();}

 		switch (la.kind) {

 		case 7: {

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

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

 					breakCount++; 

 				}

-			} else SynErr(114);

+			} else SynErr(131);

+			while (!(la.kind == 0 || la.kind == 17)) {SynErr(132); Get();}

 			Expect(17);

 			s = label != null ? new BreakStmt(x, label) : new BreakStmt(x, breakCount); 

 			break;

@@ -1022,7 +1040,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			ReturnStmt(out s);

 			break;

 		}

-		default: SynErr(115); break;

+		default: SynErr(133); break;

 		}

 	}

 

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

 			Get();

 			SemErr(t, "invalid statement (did you forget the 'label' keyword?)"); 

-		} else SynErr(116);

+		} else SynErr(134);

 		s = new UpdateStmt(x, lhss, rhss); 

 	}

 

@@ -1134,13 +1152,13 @@ List<Expression/*!*/>/*!*/ decreases) {
 		Expect(17);

 		UpdateStmt update;

 		if (rhss.Count == 0) {

-		  update = null;

+		 update = null;

 		} else {

-		  var ies = new List<Expression>();

-		  foreach (var lhs in lhss) {

-		    ies.Add(new AutoGhostIdentifierExpr(lhs.Tok, lhs.Name));

-		  }

-		  update = new UpdateStmt(assignTok, ies, rhss);

+		 var ies = new List<Expression>();

+		 foreach (var lhs in lhss) {

+		   ies.Add(new AutoGhostIdentifierExpr(lhs.Tok, lhs.Name));

+		 }

+		 update = new UpdateStmt(assignTok, ies, rhss);

 		}

 		s = new VarDeclStmt(x, lhss, update);

 		

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

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

 					els = s; 

-				} else SynErr(117);

+				} else SynErr(135);

 			}

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

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

 			AlternativeBlock(out alternatives);

 			ifStmt = new AlternativeStmt(x, alternatives); 

-		} else SynErr(118);

+		} else SynErr(136);

 	}

 

 	void WhileStmt(out Statement/*!*/ stmt) {

@@ -1197,11 +1215,11 @@ List<Expression/*!*/>/*!*/ decreases) {
 			LoopSpec(out invariants, out decreases, out mod);

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

 			stmt = new WhileStmt(x, guard, invariants, decreases, mod, body); 

-		} else if (StartOf(9)) {

+		} else if (StartOf(12)) {

 			LoopSpec(out invariants, out decreases, out mod);

 			AlternativeBlock(out alternatives);

 			stmt = new AlternativeLoopStmt(x, invariants, decreases, mod, alternatives); 

-		} else SynErr(119);

+		} else SynErr(137);

 	}

 

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

@@ -1260,7 +1278,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		

 		Expect(48);

 		returnTok = t; 

-		if (StartOf(10)) {

+		if (StartOf(13)) {

 			Rhs(out r, null);

 			rhss = new List<AssignmentRhs>(); rhss.Add(r); 

 			while (la.kind == 19) {

@@ -1298,7 +1316,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 					Ident(out x);

 					Expect(33);

 					args = new List<Expression/*!*/>(); 

-					if (StartOf(6)) {

+					if (StartOf(8)) {

 						Expressions(args);

 					}

 					Expect(34);

@@ -1309,7 +1327,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			if (ee != null) {

 			 r = new TypeRhs(newToken, ty, ee);

 			} else {

-			  r = new TypeRhs(newToken, ty, initCall);

+			 r = new TypeRhs(newToken, ty, initCall);

 			}

 			

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

@@ -1320,10 +1338,10 @@ List<Expression/*!*/>/*!*/ decreases) {
 		} else if (la.kind == 44) {

 			Get();

 			r = new HavocRhs(t); 

-		} else if (StartOf(6)) {

+		} else if (StartOf(8)) {

 			Expression(out e);

 			r = new ExprRhs(e); 

-		} else SynErr(120);

+		} else SynErr(138);

 	}

 

 	void Lhs(out Expression e) {

@@ -1334,13 +1352,13 @@ List<Expression/*!*/>/*!*/ decreases) {
 			while (la.kind == 51 || la.kind == 53) {

 				Suffix(ref e);

 			}

-		} else if (StartOf(11)) {

+		} else if (StartOf(14)) {

 			ConstAtomExpression(out e);

 			Suffix(ref e);

 			while (la.kind == 51 || la.kind == 53) {

 				Suffix(ref e);

 			}

-		} else SynErr(121);

+		} else SynErr(139);

 	}

 

 	void Expressions(List<Expression/*!*/>/*!*/ args) {

@@ -1360,10 +1378,10 @@ List<Expression/*!*/>/*!*/ decreases) {
 		if (la.kind == 44) {

 			Get();

 			e = null; 

-		} else if (StartOf(6)) {

+		} else if (StartOf(8)) {

 			Expression(out ee);

 			e = ee; 

-		} else SynErr(122);

+		} else SynErr(140);

 		Expect(34);

 	}

 

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

 			Expect(58);

 			body = new List<Statement>(); 

-			while (StartOf(7)) {

+			while (StartOf(9)) {

 				Stmt(body);

 			}

 			alternatives.Add(new GuardedAlternative(x, e, body)); 

@@ -1389,30 +1407,29 @@ List<Expression/*!*/>/*!*/ decreases) {
 	}

 

 	void LoopSpec(out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!*/> decreases, out List<FrameExpression/*!*/> mod) {

-		bool isFree;  Expression/*!*/ e; FrameExpression/*!*/ fe;

+		FrameExpression/*!*/ fe;

 		invariants = new List<MaybeFreeExpression/*!*/>();

+		MaybeFreeExpression invariant = null;

 		decreases = new List<Expression/*!*/>();

 		mod = null;

 		

-		while (StartOf(12)) {

+		while (StartOf(15)) {

 			if (la.kind == 29 || la.kind == 60) {

-				isFree = false; 

-				if (la.kind == 29) {

-					Get();

-					isFree = true; 

-				}

-				Expect(60);

-				Expression(out e);

-				invariants.Add(new MaybeFreeExpression(e, isFree)); 

+				Invariant(out invariant);

+				while (!(la.kind == 0 || la.kind == 17)) {SynErr(141); Get();}

 				Expect(17);

+				invariants.Add(invariant); 

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

+				while (!(la.kind == 0 || la.kind == 32)) {SynErr(142); Get();}

 				Get();

 				DecreasesList(decreases, true);

+				while (!(la.kind == 0 || la.kind == 17)) {SynErr(143); Get();}

 				Expect(17);

 			} else {

+				while (!(la.kind == 0 || la.kind == 28)) {SynErr(144); Get();}

 				Get();

 				mod = mod ?? new List<FrameExpression>(); 

-				if (StartOf(6)) {

+				if (StartOf(8)) {

 					FrameExpression(out fe);

 					mod.Add(fe); 

 					while (la.kind == 19) {

@@ -1421,11 +1438,24 @@ List<Expression/*!*/>/*!*/ decreases) {
 						mod.Add(fe); 

 					}

 				}

+				while (!(la.kind == 0 || la.kind == 17)) {SynErr(145); Get();}

 				Expect(17);

 			}

 		}

 	}

 

+	void Invariant(out MaybeFreeExpression/*!*/ invariant) {

+		bool isFree = false; Expression/*!*/ e; invariant = null; 

+		while (!(la.kind == 0 || la.kind == 29 || la.kind == 60)) {SynErr(146); Get();}

+		if (la.kind == 29) {

+			Get();

+			isFree = true; 

+		}

+		Expect(60);

+		Expression(out e);

+		invariant = new MaybeFreeExpression(e, isFree); 

+	}

+

 	void CaseStatement(out MatchCaseStmt/*!*/ c) {

 		Contract.Ensures(Contract.ValueAtReturn(out c) != null);

 		IToken/*!*/ x, id;

@@ -1448,7 +1478,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Expect(34);

 		}

 		Expect(58);

-		while (StartOf(7)) {

+		while (StartOf(9)) {

 			Stmt(body);

 		}

 		c = new MatchCaseStmt(x, id.val, arguments, body); 

@@ -1459,10 +1489,10 @@ List<Expression/*!*/>/*!*/ decreases) {
 		if (la.kind == 4) {

 			Get();

 			arg = new Attributes.Argument(t, t.val.Substring(1, t.val.Length-2)); 

-		} else if (StartOf(6)) {

+		} else if (StartOf(8)) {

 			Expression(out e);

 			arg = new Attributes.Argument(t, e); 

-		} else SynErr(123);

+		} else SynErr(147);

 	}

 

 	void QuantifierDomain(out List<BoundVar/*!*/> bvars, out Attributes attrs, out Expression range) {

@@ -1514,13 +1544,13 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Get();

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

 			Get();

-		} else SynErr(124);

+		} else SynErr(148);

 	}

 

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

 		Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x;  Expression/*!*/ e1; 

 		RelationalExpression(out e0);

-		if (StartOf(13)) {

+		if (StartOf(16)) {

 			if (la.kind == 70 || la.kind == 71) {

 				AndOp();

 				x = t; 

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

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

 			Get();

-		} else SynErr(125);

+		} else SynErr(149);

 	}

 

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

@@ -1561,23 +1591,23 @@ List<Expression/*!*/>/*!*/ decreases) {
 		List<Expression> chain = null;

 		List<BinaryExpr.Opcode> ops = null;

 		int kind = 0;  // 0 ("uncommitted") indicates chain of ==, possibly with one !=

-		               // 1 ("ascending")   indicates chain of ==, <, <=, possibly with one !=

-		               // 2 ("descending")  indicates chain of ==, >, >=, possibly with one !=

-		               // 3 ("illegal")     indicates illegal chain

-		               // 4 ("disjoint")    indicates chain of disjoint set operators

+		              // 1 ("ascending")   indicates chain of ==, <, <=, possibly with one !=

+		              // 2 ("descending")  indicates chain of ==, >, >=, possibly with one !=

+		              // 3 ("illegal")     indicates illegal chain

+		              // 4 ("disjoint")    indicates chain of disjoint set operators

 		bool hasSeenNeq = false;

 		

 		Term(out e0);

 		e = e0; 

-		if (StartOf(14)) {

+		if (StartOf(17)) {

 			RelOp(out x, out op);

 			firstOpTok = x; 

 			Term(out e1);

 			e = new BinaryExpr(x, op, e0, e1);

 			if (op == BinaryExpr.Opcode.Disjoint)

-			  acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, e0, e1); // accumulate first two operands.

+			 acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, e0, e1); // accumulate first two operands.

 			

-			while (StartOf(14)) {

+			while (StartOf(17)) {

 				if (chain == null) {

 				 chain = new List<Expression>();

 				 ops = new List<BinaryExpr.Opcode>();

@@ -1631,11 +1661,11 @@ List<Expression/*!*/>/*!*/ decreases) {
 				Term(out e1);

 				ops.Add(op); chain.Add(e1);

 				if (op == BinaryExpr.Opcode.Disjoint) {

-				  e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, acc, e1));

-				  acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, acc, e1); //e0 has already been added.

+				 e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, acc, e1));

+				 acc = new BinaryExpr(x, BinaryExpr.Opcode.Add, acc, e1); //e0 has already been added.

 				}

 				else

-				  e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, e0, e1));

+				 e = new BinaryExpr(x, BinaryExpr.Opcode.And, e, new BinaryExpr(x, op, e0, e1));

 				

 			}

 		}

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

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

 			Get();

-		} else SynErr(126);

+		} else SynErr(150);

 	}

 

 	void OrOp() {

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

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

 			Get();

-		} else SynErr(127);

+		} else SynErr(151);

 	}

 

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

@@ -1727,10 +1757,10 @@ List<Expression/*!*/>/*!*/ decreases) {
 			if (y == Token.NoToken) {

 			 SemErr(x, "invalid RelOp");

 			} else if (y.pos != x.pos + 1) {

-			  SemErr(x, "invalid RelOp (perhaps you intended \"!in\" with no intervening whitespace?)");

+			 SemErr(x, "invalid RelOp (perhaps you intended \"!in\" with no intervening whitespace?)");

 			} else {

-			  x.val = "!in";

-			  op = BinaryExpr.Opcode.NotIn;

+			 x.val = "!in";

+			 op = BinaryExpr.Opcode.NotIn;

 			}

 			

 			break;

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

 			break;

 		}

-		default: SynErr(128); break;

+		default: SynErr(152); break;

 		}

 	}

 

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

 			Get();

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

-		} else SynErr(129);

+		} else SynErr(153);

 	}

 

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

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

 			break;

 		}

-		default: SynErr(130); break;

+		default: SynErr(154); break;

 		}

 	}

 

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

 			Get();

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

-		} else SynErr(131);

+		} else SynErr(155);

 	}

 

 	void NegOp() {

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

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

 			Get();

-		} else SynErr(132);

+		} else SynErr(156);

 	}

 

 	void EndlessExpression(out Expression e) {

@@ -1918,7 +1948,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			e = new LetExpr(x, letVars, letRHSs, e); 

 			break;

 		}

-		default: SynErr(133); break;

+		default: SynErr(157); break;

 		}

 	}

 

@@ -1937,7 +1967,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		if (la.kind == 33) {

 			Get();

 			openParen = t;  args = new List<Expression>(); 

-			if (StartOf(6)) {

+			if (StartOf(8)) {

 				Expressions(args);

 			}

 			Expect(34);

@@ -1957,7 +1987,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			if (la.kind == 33) {

 				Get();

 				args = new List<Expression/*!*/>();  func = true; 

-				if (StartOf(6)) {

+				if (StartOf(8)) {

 					Expressions(args);

 				}

 				Expect(34);

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

 			Get();

 			x = t; 

-			if (StartOf(6)) {

+			if (StartOf(8)) {

 				Expression(out ee);

 				e0 = ee; 

 				if (la.kind == 97) {

 					Get();

 					anyDots = true; 

-					if (StartOf(6)) {

+					if (StartOf(8)) {

 						Expression(out ee);

 						e1 = ee; 

 					}

@@ -1992,39 +2022,39 @@ List<Expression/*!*/>/*!*/ decreases) {
 						multipleIndices.Add(ee);

 						

 					}

-				} else SynErr(134);

+				} else SynErr(158);

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

 				Get();

 				anyDots = true; 

-				if (StartOf(6)) {

+				if (StartOf(8)) {

 					Expression(out ee);

 					e1 = ee; 

 				}

-			} else SynErr(135);

+			} else SynErr(159);

 			if (multipleIndices != null) {

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

 			 // make sure an array class with this dimensionality exists

 			 UserDefinedType tmp = theBuiltIns.ArrayType(x, multipleIndices.Count, new IntType(), true);

 			} else {

-			  if (!anyDots && e0 == null) {

-			    /* a parsing error occurred */

-			    e0 = dummyExpr;

-			  }

-			  Contract.Assert(anyDots || e0 != null);

-			  if (anyDots) {

-			    //Contract.Assert(e0 != null || e1 != null);

-			    e = new SeqSelectExpr(x, false, e, e0, e1);

-			  } else if (e1 == null) {

-			    Contract.Assert(e0 != null);

-			    e = new SeqSelectExpr(x, true, e, e0, null);

-			  } else {

-			    Contract.Assert(e0 != null);

-			    e = new SeqUpdateExpr(x, e, e0, e1);

-			  }

+			 if (!anyDots && e0 == null) {

+			   /* a parsing error occurred */

+			   e0 = dummyExpr;

+			 }

+			 Contract.Assert(anyDots || e0 != null);

+			 if (anyDots) {

+			   //Contract.Assert(e0 != null || e1 != null);

+			   e = new SeqSelectExpr(x, false, e, e0, e1);

+			 } else if (e1 == null) {

+			   Contract.Assert(e0 != null);

+			   e = new SeqSelectExpr(x, true, e, e0, null);

+			 } else {

+			   Contract.Assert(e0 != null);

+			   e = new SeqUpdateExpr(x, e, e0, e1);

+			 }

 			}

 			

 			Expect(52);

-		} else SynErr(136);

+		} else SynErr(160);

 	}

 

 	void DisplayExpr(out Expression e) {

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

 			Get();

 			x = t;  elements = new List<Expression/*!*/>(); 

-			if (StartOf(6)) {

+			if (StartOf(8)) {

 				Expressions(elements);

 			}

 			e = new SetDisplayExpr(x, elements);

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

 			Get();

 			x = t;  elements = new List<Expression/*!*/>(); 

-			if (StartOf(6)) {

+			if (StartOf(8)) {

 				Expressions(elements);

 			}

 			e = new SeqDisplayExpr(x, elements); 

 			Expect(52);

-		} else SynErr(137);

+		} else SynErr(161);

 	}

 

 	void MultiSetExpr(out Expression e) {

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

 			Get();

 			elements = new List<Expression/*!*/>(); 

-			if (StartOf(6)) {

+			if (StartOf(8)) {

 				Expressions(elements);

 			}

 			e = new MultiSetDisplayExpr(x, elements);

@@ -2072,9 +2102,9 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Expression(out e);

 			e = new MultiSetFormingExpr(x, e); 

 			Expect(34);

-		} else if (StartOf(15)) {

+		} else if (StartOf(18)) {

 			SemErr("multiset must be followed by multiset literal or expression to coerce in parentheses."); 

-		} else SynErr(138);

+		} else SynErr(162);

 	}

 

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

@@ -2151,7 +2181,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			Expect(34);

 			break;

 		}

-		default: SynErr(139); break;

+		default: SynErr(163); break;

 		}

 	}

 

@@ -2160,8 +2190,8 @@ List<Expression/*!*/>/*!*/ decreases) {
 		try {

 		 n = BigInteger.Parse(t.val);

 		} catch (System.FormatException) {

-		  SemErr("incorrectly formatted number");

-		  n = BigInteger.Zero;

+		 SemErr("incorrectly formatted number");

+		 n = BigInteger.Zero;

 		}

 		

 	}

@@ -2194,14 +2224,14 @@ List<Expression/*!*/>/*!*/ decreases) {
 		} else if (la.kind == 100 || la.kind == 101) {

 			Exists();

 			x = t; 

-		} else SynErr(140);

+		} else SynErr(164);

 		QuantifierDomain(out bvars, out attrs, out range);

 		QSep();

 		Expression(out body);

 		if (univ) {

 		 q = new ForallExpr(x, bvars, range, body, attrs);

 		} else {

-		  q = new ExistsExpr(x, bvars, range, body, attrs);

+		 q = new ExistsExpr(x, bvars, range, body, attrs);

 		}

 		

 	}

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

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

 			Get();

-		} else SynErr(141);

+		} else SynErr(165);

 	}

 

 	void Exists() {

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

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

 			Get();

-		} else SynErr(142);

+		} else SynErr(166);

 	}

 

 	void QSep() {

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

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

 			Get();

-		} else SynErr(143);

+		} else SynErr(167);

 	}

 

 	void AttributeBody(ref Attributes attrs) {

@@ -2291,7 +2321,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		Expect(22);

 		Expect(1);

 		aName = t.val; 

-		if (StartOf(16)) {

+		if (StartOf(19)) {

 			AttributeArg(out aArg);

 			aArgs.Add(aArg); 

 			while (la.kind == 19) {

@@ -2307,23 +2337,27 @@ List<Expression/*!*/>/*!*/ decreases) {
 

 	public void Parse() {

 		la = new Token();

-		la.val = "";		

+		la.val = "";

 		Get();

 		Dafny();

+		Expect(0);

 

-    Expect(0);

+		Expect(0);

 	}

-	

+

 	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},

+		{T,T,T,x, x,x,x,T, x,T,T,T, x,x,T,x, T,T,T,x, x,x,x,x, x,T,T,x, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,x,x,x, x,x,x,T, x,x,x,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,T,T,T, T,T,T,T, 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, x,x,T,x, T,x,x,x, x,T,T,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,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,T,x, T,x,x,x, x,T,T,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,x,x, x,x,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,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},

+		{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,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, 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,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, x,x,x,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, x,x,x,x, x,x,x,x, x,x,x,x, x,x,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, 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,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},

 		{x,T,T,x, x,x,x,T, x,x,x,T, x,x,x,x, T,x,T,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,T,T, T,x,x,x, x,x,x,T, x,x,x,T, 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,T,T,T, T,T,T,T, 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, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, T,x,x,x, x,x,x,T, x,x,x,T, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, x,x},

+		{T,T,T,x, x,x,x,T, x,x,x,T, x,x,x,x, T,x,T,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,T,T, T,x,x,x, x,x,x,T, x,x,x,T, 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,T,T,T, T,T,T,T, 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, T,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,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,T,T,x, x,x,x,T, x,x,x,x, x,x,x,x, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, x,x,x,x, T,x,x,x, x,x,T,T, x,x,T,T, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,x,x, T,T,T,T, T,T,T,T, x,x,T,T, T,T,x,x, 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,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,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x},

@@ -2340,18 +2374,20 @@ List<Expression/*!*/>/*!*/ decreases) {
 public class Errors {

 	public int count = 0;                                    // number of errors detected

 	public System.IO.TextWriter/*!*/ errorStream = Console.Out;   // error messages go to this stream

-  public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text

-  public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text

-  

+	public string errMsgFormat = "{0}({1},{2}): error: {3}"; // 0=filename, 1=line, 2=column, 3=text

+	public string warningMsgFormat = "{0}({1},{2}): warning: {3}"; // 0=filename, 1=line, 2=column, 3=text

+

 	public void SynErr(string filename, int line, int col, int n) {

-    SynErr(filename, line, col, GetSyntaxErrorString(n));

-  }

-	public virtual void SynErr(string filename, int line, int col, string msg) {

-	  Contract.Requires(msg != null);

+		SynErr(filename, line, col, GetSyntaxErrorString(n));

+	}

+

+	public virtual void SynErr(string filename, int line, int col, string/*!*/ msg) {

+		Contract.Requires(msg != null);

 		errorStream.WriteLine(errMsgFormat, filename, line, col, msg);

 		count++;

-  }

-  string GetSyntaxErrorString(int n) {

+	}

+

+	string GetSyntaxErrorString(int n) {

 		string s;

 		switch (n) {

 			case 0: s = "EOF expected"; break;

@@ -2459,49 +2495,73 @@ public class Errors {
 			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 MethodDecl"; break;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

-			case 137: s = "invalid DisplayExpr"; break;

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

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

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

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

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

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

+			case 105: s = "this symbol not expected in ClassDecl"; break;

+			case 106: s = "this symbol not expected in DatatypeDecl"; break;

+			case 107: s = "this symbol not expected in DatatypeDecl"; break;

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

+			case 109: s = "this symbol not expected in FieldDecl"; break;

+			case 110: s = "this symbol not expected in FieldDecl"; break;

+			case 111: s = "this symbol not expected in MethodDecl"; break;

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

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

+			case 114: s = "this symbol not expected in MethodSpec"; break;

+			case 115: s = "this symbol not expected in MethodSpec"; break;

+			case 116: s = "this symbol not expected in MethodSpec"; break;

+			case 117: s = "this symbol not expected in MethodSpec"; break;

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

+			case 119: s = "this symbol not expected in MethodSpec"; break;

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

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

+			case 122: s = "this symbol not expected in FunctionSpec"; break;

+			case 123: s = "this symbol not expected in FunctionSpec"; break;

+			case 124: s = "this symbol not expected in FunctionSpec"; break;

+			case 125: s = "this symbol not expected in FunctionSpec"; break;

+			case 126: s = "this symbol not expected in FunctionSpec"; break;

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

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

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

+			case 130: s = "this symbol not expected in OneStmt"; break;

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

+			case 132: s = "this symbol not expected in OneStmt"; break;

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

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

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

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

+			case 137: s = "invalid WhileStmt"; break;

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

+			case 139: s = "invalid Lhs"; break;

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

+			case 141: s = "this symbol not expected in LoopSpec"; break;

+			case 142: s = "this symbol not expected in LoopSpec"; break;

+			case 143: s = "this symbol not expected in LoopSpec"; break;

+			case 144: s = "this symbol not expected in LoopSpec"; break;

+			case 145: s = "this symbol not expected in LoopSpec"; break;

+			case 146: s = "this symbol not expected in Invariant"; break;

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

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

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

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

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

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

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

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

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

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

+			case 157: s = "invalid EndlessExpression"; break;

+			case 158: s = "invalid Suffix"; break;

+			case 159: s = "invalid Suffix"; break;

+			case 160: s = "invalid Suffix"; break;

+			case 161: s = "invalid DisplayExpr"; break;

+			case 162: s = "invalid MultiSetExpr"; break;

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

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

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

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

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

 

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

 		}

-    return s;

+		return s;

 	}

 

 	public void SemErr(IToken/*!*/ tok, string/*!*/ msg) {  // semantic errors

@@ -2509,8 +2569,9 @@ public class Errors {
 		Contract.Requires(msg != null);

 		SemErr(tok.filename, tok.line, tok.col, msg);

 	}

+

 	public virtual void SemErr(string filename, int line, int col, string/*!*/ msg) {

-	  Contract.Requires(msg != null);

+		Contract.Requires(msg != null);

 		errorStream.WriteLine(errMsgFormat, filename, line, col, msg);

 		count++;

 	}

@@ -2526,4 +2587,5 @@ public class FatalError: Exception {
 	public FatalError(string m): base(m) {}

 }

 

+

 }
\ No newline at end of file
diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs
index 1ab06974..f0eb1937 100644
--- a/Source/Dafny/Scanner.cs
+++ b/Source/Dafny/Scanner.cs
@@ -19,7 +19,7 @@ public class Buffer {
 	//    a) whole stream in buffer

 	//    b) part of stream in buffer

 	// 2) non seekable stream (network, console)

-  

+

 	public const int EOF = 65535 + 1; // char.MaxValue + 1;

 	const int MIN_BUFFER_LENGTH = 1024; // 1KB

 	const int MAX_BUFFER_LENGTH = MIN_BUFFER_LENGTH * 64; // 64KB

@@ -31,15 +31,17 @@ public class Buffer {
 	Stream/*!*/ stream;      // input stream (seekable)

 	bool isUserStream;  // was the stream opened by the user?

 

-[ContractInvariantMethod]

-void ObjectInvariant(){

-  Contract.Invariant(buf != null);

-  Contract.Invariant(stream != null);}

-    [NotDelayed]

-	public Buffer (Stream/*!*/ s, bool isUserStream) :base() {

+	[ContractInvariantMethod]

+	void ObjectInvariant(){

+		Contract.Invariant(buf != null);

+		Contract.Invariant(stream != null);

+	}

+

+//  [NotDelayed]

+	public Buffer (Stream/*!*/ s, bool isUserStream) : base() {

 	  Contract.Requires(s != null);

 		stream = s; this.isUserStream = isUserStream;

-		

+

 		int fl, bl;

 		if (s.CanSeek) {

 			fl = (int) s.Length;

@@ -51,12 +53,12 @@ void ObjectInvariant(){
 

 		buf = new byte[(bl>0) ? bl : MIN_BUFFER_LENGTH];

 		fileLen = fl;  bufLen = bl;

-		

+

 		if (fileLen > 0) Pos = 0; // setup buffer to position 0 (start)

 		else bufPos = 0; // index 0 is already after the file, thus Pos = 0 is invalid

 		if (bufLen == fileLen && s.CanSeek) Close();

 	}

-	

+

 	protected Buffer(Buffer/*!*/ b) { // called in UTF8Buffer constructor

 	  Contract.Requires(b != null);

 		buf = b.buf;

@@ -73,14 +75,14 @@ void ObjectInvariant(){
 	}

 

 	~Buffer() { Close(); }

-	

+

 	protected void Close() {

 		if (!isUserStream && stream != null) {

 			stream.Close();

 			//stream = null;

 		}

 	}

-	

+

 	public virtual int Read () {

 		if (bufPos < bufLen) {

 			return buf[bufPos++];

@@ -100,7 +102,7 @@ void ObjectInvariant(){
 		Pos = curPos;

 		return ch;

 	}

-	

+

 	public string/*!*/ GetString (int beg, int end) {

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

 		int len = 0;

@@ -139,7 +141,7 @@ void ObjectInvariant(){
 			}

 		}

 	}

-	

+

 	// Read the next chunk of bytes from the stream, increases the buffer

 	// if needed and updates the fields fileLen and bufLen.

 	// Returns the number of bytes read.

@@ -213,22 +215,24 @@ public class Scanner {
 	const int noSym = 104;

 

 

-[ContractInvariantMethod]

-void objectInvariant(){

-  Contract.Invariant(buffer!=null);

-  Contract.Invariant(t != null);

-  Contract.Invariant(start != null);

-  Contract.Invariant(tokens != null);

-  Contract.Invariant(pt != null);

-  Contract.Invariant(tval != null);

-  Contract.Invariant(Filename != null);

-  Contract.Invariant(errorHandler != null);

-}

+	[ContractInvariantMethod]

+	void objectInvariant(){

+		Contract.Invariant(buffer!=null);

+		Contract.Invariant(t != null);

+		Contract.Invariant(start != null);

+		Contract.Invariant(tokens != null);

+		Contract.Invariant(pt != null);

+		Contract.Invariant(tval != null);

+		Contract.Invariant(Filename != null);

+		Contract.Invariant(errorHandler != null);

+	}

+

 	public Buffer/*!*/ buffer; // scanner buffer

-	

+

 	Token/*!*/ t;          // current token

 	int ch;           // current input character

 	int pos;          // byte position of current character

+	int charPos;

 	int col;          // column number of current character

 	int line;         // line number of current character

 	int oldEols;      // EOLs that appeared in a comment;

@@ -236,13 +240,13 @@ void objectInvariant(){
 

 	Token/*!*/ tokens;     // list of tokens already peeked (first token is a dummy)

 	Token/*!*/ pt;         // current peek token

-	

+

 	char[]/*!*/ tval = new char[128]; // text of current token

 	int tlen;         // length of current token

-	

+

 	private string/*!*/ Filename;

 	private Errors/*!*/ errorHandler;

-	

+

 	static Scanner() {

 		start = new Hashtable(128);

 		for (int i = 39; i <= 39; ++i) start[i] = 1;

@@ -290,9 +294,9 @@ void objectInvariant(){
 		start[Buffer.EOF] = -1;

 

 	}

-	

-	[NotDelayed]

-	public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler) :base(){

+

+//	[NotDelayed]

+	public Scanner (string/*!*/ fileName, Errors/*!*/ errorHandler) : base() {

 	  Contract.Requires(fileName != null);

 	  Contract.Requires(errorHandler != null);

 		this.errorHandler = errorHandler;

@@ -302,15 +306,14 @@ void objectInvariant(){
 			Stream stream = new FileStream(fileName, FileMode.Open, FileAccess.Read, FileShare.Read);

 			buffer = new Buffer(stream, false);

 			Filename = fileName;

-			

 			Init();

 		} catch (IOException) {

 			throw new FatalError("Cannot open file " + fileName);

 		}

 	}

-	

-	[NotDelayed]

-	public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName) :base(){

+

+//	[NotDelayed]

+	public Scanner (Stream/*!*/ s, Errors/*!*/ errorHandler, string/*!*/ fileName) : base() {

 	  Contract.Requires(s != null);

 	  Contract.Requires(errorHandler != null);

 	  Contract.Requires(fileName != null);

@@ -319,10 +322,9 @@ void objectInvariant(){
 		buffer = new Buffer(s, true);

 		this.errorHandler = errorHandler;

 		this.Filename = fileName;

-		

 		Init();

 	}

-	

+

 	void Init() {

 		pos = -1; line = 1; col = 0;

 		oldEols = 0;

@@ -343,11 +345,11 @@ void objectInvariant(){
 	Contract.Ensures(Contract.Result<string>() != null);

 	  int p = buffer.Pos;

 	  int ch = buffer.Read();

-      // replace isolated '\r' by '\n' in order to make

+	  // replace isolated '\r' by '\n' in order to make

 	  // eol handling uniform across Windows, Unix and Mac

 	  if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;

 	  while (ch != EOL && ch != Buffer.EOF){

-	    ch = buffer.Read();

+		ch = buffer.Read();

 		// replace isolated '\r' by '\n' in order to make

 		// eol handling uniform across Windows, Unix and Mac

 		if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;

@@ -358,7 +360,7 @@ void objectInvariant(){
 	}

 

 	void NextCh() {

-		if (oldEols > 0) { ch = EOL; oldEols--; } 

+		if (oldEols > 0) { ch = EOL; oldEols--; }

 		else {

 //			pos = buffer.Pos;

 //			ch = buffer.Read(); col++;

@@ -366,9 +368,9 @@ void objectInvariant(){
 //			// eol handling uniform across Windows, Unix and Mac

 //			if (ch == '\r' && buffer.Peek() != '\n') ch = EOL;

 //			if (ch == EOL) { line++; col = 0; }

-			

+

 			while (true) {

-			    pos = buffer.Pos;

+				pos = buffer.Pos;

 				ch = buffer.Read(); col++;

 				// replace isolated '\r' by '\n' in order to make

 				// eol handling uniform across Windows, Unix and Mac

@@ -418,7 +420,7 @@ void objectInvariant(){
 				return;

 			  }

 

-			

+

 		}

 

 	}

@@ -438,7 +440,7 @@ void objectInvariant(){
 

 

 	bool Comment0() {

-		int level = 1, pos0 = pos, line0 = line, col0 = col;

+		int level = 1, pos0 = pos, line0 = line, col0 = col, charPos0 = charPos;

 		NextCh();

 		if (ch == '/') {

 			NextCh();

@@ -451,13 +453,13 @@ void objectInvariant(){
 				else NextCh();

 			}

 		} else {

-			buffer.Pos = pos0; NextCh(); line = line0; col = col0;

+			buffer.Pos = pos0; NextCh(); line = line0; col = col0; charPos = charPos0;

 		}

 		return false;

 	}

 

 	bool Comment1() {

-		int level = 1, pos0 = pos, line0 = line, col0 = col;

+		int level = 1, pos0 = pos, line0 = line, col0 = col, charPos0 = charPos;

 		NextCh();

 		if (ch == '*') {

 			NextCh();

@@ -478,7 +480,7 @@ void objectInvariant(){
 				else NextCh();

 			}

 		} else {

-			buffer.Pos = pos0; NextCh(); line = line0; col = col0;

+			buffer.Pos = pos0; NextCh(); line = line0; col = col0; charPos = charPos0;

 		}

 		return false;

 	}

@@ -556,10 +558,13 @@ void objectInvariant(){
 		t.pos = pos; t.col = col; t.line = line;

 		t.filename = this.Filename;

 		int state;

-		if (start.ContainsKey(ch)) { state = (int) cce.NonNull( start[ch]); }

+		if (start.ContainsKey(ch)) {

+			Contract.Assert(start[ch] != null);

+			state = (int) start[ch];

+		}

 		else { state = 0; }

 		tlen = 0; AddCh();

-		

+

 		switch (state) {

 			case -1: { t.kind = eofSym; break; } // NextCh already done

 			case 0: {

@@ -759,14 +764,14 @@ void objectInvariant(){
 		t.val = new String(tval, 0, tlen);

 		return t;

 	}

-	

+

 	private void SetScannerBehindT() {

 		buffer.Pos = t.pos;

 		NextCh();

 		line = t.line; col = t.col;

 		for (int i = 0; i < tlen; i++) NextCh();

 	}

-	

+

 	// get the next token (possibly a token already seen during peeking)

 	public Token/*!*/ Scan () {

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

@@ -787,7 +792,7 @@ void objectInvariant(){
 			}

 			pt = pt.next;

 		} while (pt.kind > maxT); // skip pragmas

-	

+

 		return pt;

 	}