Added loop modifies clause syntax.

4 files changed, 129 insertions, 97 deletions

diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg
index 071dbd64..e117ad67 100644
--- a/Dafny/Dafny.atg
+++ b/Dafny/Dafny.atg
@@ -843,6 +843,7 @@ WhileStmt<out Statement/*!*/ stmt>
      Expression guard;

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

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

+     List<FrameExpression/*!*/> mod = new List<FrameExpression/*!*/>();

      Statement/*!*/ body;

      IToken bodyStart, bodyEnd;

      List<GuardedAlternative> alternatives;

@@ -851,20 +852,21 @@ WhileStmt<out Statement/*!*/ stmt>
   "while"                    (. x = t; .)

   (

     Guard<out guard>           (. Contract.Assume(guard == null || cce.Owner.None(guard)); .)

-    LoopSpec<out invariants, out decreases>

+    LoopSpec<out invariants, out decreases, out mod>

     BlockStmt<out body, out bodyStart, out bodyEnd>

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

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

   |

-    LoopSpec<out invariants, out decreases>

+    LoopSpec<out invariants, out decreases, out mod>

     AlternativeBlock<out alternatives>

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

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

   )

   .

 

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

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

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

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

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

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

+     mod = new List<FrameExpression/*!*/>();

   .)

   {                         (. isFree = false; .)

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

@@ -873,6 +875,10 @@ LoopSpec<.out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!*
     Expression<out e>       (. invariants.Add(new MaybeFreeExpression(e, isFree)); .)

     ";"

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

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

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

+                 }

+               ] ";"

   }

   .

 

diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs
index 99cf791f..dc925519 100644
--- a/Dafny/DafnyAst.cs
+++ b/Dafny/DafnyAst.cs
@@ -1660,20 +1660,24 @@ namespace Microsoft.Dafny {
   {

     public readonly List<MaybeFreeExpression/*!*/>/*!*/ Invariants;

     public readonly List<Expression/*!*/>/*!*/ Decreases;

+    public readonly List<FrameExpression/*!*/>/*!*/ Mod;

     [ContractInvariantMethod]

     void ObjectInvariant() {

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

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

+      Contract.Invariant(cce.NonNullElements(Mod));

     }

-    public LoopStmt(IToken tok, List<MaybeFreeExpression/*!*/>/*!*/ invariants, List<Expression/*!*/>/*!*/ decreases)

+    public LoopStmt(IToken tok, List<MaybeFreeExpression/*!*/>/*!*/ invariants, List<Expression/*!*/>/*!*/ decreases, List<FrameExpression/*!*/>/*!*/ mod)

     : base(tok) 

     {

       Contract.Requires(tok != null);

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

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

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

 

       this.Invariants = invariants;

       this.Decreases = decreases;

+      this.Mod = mod;

     }

   }

 

@@ -1687,9 +1691,9 @@ namespace Microsoft.Dafny {
     }

 

     public WhileStmt(IToken tok, Expression guard,

-                     List<MaybeFreeExpression/*!*/>/*!*/ invariants, List<Expression/*!*/>/*!*/ decreases,

+                     List<MaybeFreeExpression/*!*/>/*!*/ invariants, List<Expression/*!*/>/*!*/ decreases, List<FrameExpression/*!*/>/*!*/ mod,

                      Statement/*!*/ body)

-      : base(tok, invariants, decreases) {

+      : base(tok, invariants, decreases, mod) {

       Contract.Requires(tok != null);

       Contract.Requires(body != null);

       this.Guard = guard;

@@ -1705,9 +1709,9 @@ namespace Microsoft.Dafny {
       Contract.Invariant(Alternatives != null);

     }

     public AlternativeLoopStmt(IToken tok,

-                               List<MaybeFreeExpression/*!*/>/*!*/ invariants, List<Expression/*!*/>/*!*/ decreases,

+                               List<MaybeFreeExpression/*!*/>/*!*/ invariants, List<Expression/*!*/>/*!*/ decreases, List<FrameExpression/*!*/>/*!*/ mod,

                                List<GuardedAlternative> alternatives)

-      : base(tok, invariants, decreases) {

+      : base(tok, invariants, decreases, mod) {

       Contract.Requires(tok != null);

       Contract.Requires(alternatives != null);

       this.Alternatives = alternatives;

diff --git a/Dafny/Parser.cs b/Dafny/Parser.cs
index 41fc89c5..d11e8f08 100644
--- a/Dafny/Parser.cs
+++ b/Dafny/Parser.cs
@@ -25,7 +25,7 @@ public class Parser {
 	const bool T = true;

 	const bool x = false;

 	const int minErrDist = 2;

-	

+

 	public Scanner/*!*/ scanner;

 	public Errors/*!*/  errors;

 

@@ -144,10 +144,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);

 	}

 

@@ -160,15 +160,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 {

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

 	}

 

-	

+

 	void Dafny() {

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

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

@@ -1189,6 +1189,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 		Expression guard;

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

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

+		List<FrameExpression/*!*/> mod = new List<FrameExpression/*!*/>();

 		Statement/*!*/ body;

 		IToken bodyStart, bodyEnd;

 		List<GuardedAlternative> alternatives;

@@ -1199,13 +1200,13 @@ List<Expression/*!*/>/*!*/ decreases) {
 		if (la.kind == 33) {

 			Guard(out guard);

 			Contract.Assume(guard == null || cce.Owner.None(guard)); 

-			LoopSpec(out invariants, out decreases);

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

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

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

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

 		} else if (StartOf(11)) {

-			LoopSpec(out invariants, out decreases);

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

 			AlternativeBlock(out alternatives);

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

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

 		} else SynErr(121);

 	}

 

@@ -1388,12 +1389,13 @@ List<Expression/*!*/>/*!*/ decreases) {
 		Expect(8);

 	}

 

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

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

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

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

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

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

+		mod = new List<FrameExpression/*!*/>();

 		

-		while (la.kind == 29 || la.kind == 32 || la.kind == 59) {

+		while (StartOf(13)) {

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

 				isFree = false; 

 				if (la.kind == 29) {

@@ -1404,10 +1406,22 @@ List<Expression/*!*/>/*!*/ decreases) {
 				Expression(out e);

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

 				Expect(17);

-			} else {

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

 				Get();

 				DecreasesList(decreases, true);

 				Expect(17);

+			} else {

+				Get();

+				if (StartOf(8)) {

+					FrameExpression(out fe);

+					mod.Add(fe); 

+					while (la.kind == 19) {

+						Get();

+						FrameExpression(out fe);

+						mod.Add(fe); 

+					}

+				}

+				Expect(17);

 			}

 		}

 	}

@@ -1483,7 +1497,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 	void LogicalExpression(out Expression/*!*/ e0) {

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

 		RelationalExpression(out e0);

-		if (StartOf(13)) {

+		if (StartOf(14)) {

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

 				AndOp();

 				x = t; 

@@ -1531,12 +1545,12 @@ List<Expression/*!*/>/*!*/ decreases) {
 		

 		Term(out e0);

 		e = e0; 

-		if (StartOf(14)) {

+		if (StartOf(15)) {

 			RelOp(out x, out op);

 			firstOpTok = x; 

 			Term(out e1);

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

-			while (StartOf(14)) {

+			while (StartOf(15)) {

 				if (chain == null) {

 				 chain = new List<Expression>();

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

@@ -1788,7 +1802,7 @@ List<Expression/*!*/>/*!*/ decreases) {
 			e = new ITEExpr(x, e, e0, e1); 

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

 			MatchExpression(out e);

-		} else if (StartOf(15)) {

+		} else if (StartOf(16)) {

 			QuantifierGuts(out e);

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

 			ComprehensionExpr(out e);

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

 		Expect(1);

 		aName = t.val; 

-		if (StartOf(16)) {

+		if (StartOf(17)) {

 			AttributeArg(out aArg);

 			aArgs.Add(aArg); 

 			while (la.kind == 19) {

@@ -2179,13 +2193,13 @@ List<Expression/*!*/>/*!*/ decreases) {
 

 	public void Parse() {

 		la = new Token();

-		la.val = "";		

+		la.val = "";

 		Get();

 		Dafny();

 

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

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

@@ -2198,8 +2212,9 @@ List<Expression/*!*/>/*!*/ decreases) {
 		{x,T,T,x, x,x,x,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,T,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,T,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,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,T,T,T, x,x,x,x, x,x,T,x, x,x,T,x, T,T,x,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,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,T, x,x,x,x, x,x,T,x, x,x,T,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,T,T,T, x,x,T,T, T,T,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,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,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, 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,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,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},

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

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

@@ -2212,18 +2227,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;

@@ -2375,7 +2392,7 @@ public class Errors {
 

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

 		}

-    return s;

+		return s;

 	}

 

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

@@ -2383,8 +2400,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++;

 	}

diff --git a/Dafny/Scanner.cs b/Dafny/Scanner.cs
index 19157a32..81f556c8 100644
--- a/Dafny/Scanner.cs
+++ b/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,19 +215,20 @@ 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

@@ -236,13 +239,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 +293,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 +305,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 +321,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 +344,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 +359,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 +367,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 +419,7 @@ void objectInvariant(){
 				return;

 			  }

 

-			

+

 		}

 

 	}

@@ -555,10 +556,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: {

@@ -764,14 +768,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);

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

 			pt = pt.next;

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

-	

+

 		return pt;

 	}