diff options
author | chrishaw <unknown> | 2015-03-11 20:06:02 -0700 |
---|---|---|
committer | chrishaw <unknown> | 2015-03-11 20:06:02 -0700 |
commit | feee322b21fa0d83fd6e86142685f27bc6b73f8b (patch) | |
tree | 11f9f5e1ad581de22d2c6405e41639a8f020c74b /Source/Dafny/Scanner.cs | |
parent | 0af950664b011d95dc8d1bf84c193a151bbffac4 (diff) |
Allow trigger annotations in more statements and expressions
Diffstat (limited to 'Source/Dafny/Scanner.cs')
-rw-r--r-- | Source/Dafny/Scanner.cs | 19 |
1 files changed, 15 insertions, 4 deletions
diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs index d981a7a1..cbe8e6e5 100644 --- a/Source/Dafny/Scanner.cs +++ b/Source/Dafny/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
@@ -307,7 +318,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) {
@@ -322,7 +333,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();
|