diff options
| -rw-r--r-- | Source/Dafny/Dafny.atg | 2 | ||||
| -rw-r--r-- | Source/Dafny/Parser.cs | 2 | ||||
| -rw-r--r-- | Source/Dafny/Scanner.cs | 19 |
3 files changed, 17 insertions, 6 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 45018cd3..9dee1cc9 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -1147,7 +1147,7 @@ TypeAndToken<out IToken tok, out Type ty> ty = new UserDefinedType(tok, BuiltIns.TupleTypeName(dims), dims == 0 ? null : tupleArgTypes);
}
.)
- | (. Expression e; .)
+ | (. Expression e; tok = t; .)
NameSegmentForTypeName<out e>
{ "." ident (. tok = t; List<Type> typeArgs = null; .)
[ (. typeArgs = new List<Type>(); .)
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs index ffe3f7f2..d0bcef21 100644 --- a/Source/Dafny/Parser.cs +++ b/Source/Dafny/Parser.cs @@ -1609,7 +1609,7 @@ bool IsType(ref IToken pt) { break;
}
case 1: {
- Expression e;
+ Expression e; tok = t;
NameSegmentForTypeName(out e);
while (la.kind == 24) {
Get();
diff --git a/Source/Dafny/Scanner.cs b/Source/Dafny/Scanner.cs index bdcddb70..c9c163e6 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();
|