From 767544f7629a8d4eb2b8302bb77cf46c2c0d599a Mon Sep 17 00:00:00 2001
From: 0biha <unknown>
Date: Tue, 23 Dec 2014 16:57:03 +0100
Subject: Made invariant of class 'Scanner' robust by changing the design
 (replaced public field by private field + getter/setter).

---
 Source/Core/Scanner.cs | 19 +++++++++++++++----
 1 file changed, 15 insertions(+), 4 deletions(-)

(limited to 'Source/Core/Scanner.cs')

diff --git a/Source/Core/Scanner.cs b/Source/Core/Scanner.cs
index 5b5c0306..c6b15cc5 100644
--- a/Source/Core/Scanner.cs
+++ b/Source/Core/Scanner.cs
@@ -217,7 +217,7 @@ public class Scanner {
 
 	[ContractInvariantMethod]
 	void objectInvariant(){
-		Contract.Invariant(buffer!=null);
+		Contract.Invariant(this._buffer != null);
 		Contract.Invariant(t != null);
 		Contract.Invariant(start != null);
 		Contract.Invariant(tokens != null);
@@ -227,7 +227,18 @@ public class Scanner {
 		Contract.Invariant(errorHandler != null);
 	}
 
-	public Buffer/*!*/ buffer; // scanner buffer
+	private Buffer/*!*/ _buffer; // scanner buffer
+
+  public Buffer/*!*/ buffer {
+    get {
+      Contract.Ensures(Contract.Result<Buffer>() != null);
+      return this._buffer;
+    }
+    set {
+      Contract.Requires(value != null);
+      this._buffer = value;
+    }
+  }
 
 	Token/*!*/ t;          // current token
 	int ch;           // current input character
@@ -304,7 +315,7 @@ public class Scanner {
 		t = new Token(); // dummy because t is a non-null field
 		try {
 			Stream stream = new FileStream(fileName, FileMode.Open, FileAccess.Read, FileShare.Read);
-			buffer = new Buffer(stream, false);
+			this._buffer = new Buffer(stream, false);
 			Filename = useBaseName? GetBaseName(fileName): fileName;
 			Init();
 		} catch (IOException) {
@@ -319,7 +330,7 @@ public class Scanner {
 	  Contract.Requires(fileName != null);
 		pt = tokens = new Token();  // first token is a dummy
 		t = new Token(); // dummy because t is a non-null field
-		buffer = new Buffer(s, true);
+    this._buffer = new Buffer(s, true);
 		this.errorHandler = errorHandler;
 		this.Filename = useBaseName? GetBaseName(fileName) : fileName;
 		Init();
-- 
cgit v1.2.3