diff options
| -rw-r--r-- | Source/Dafny/Dafny.atg | 6 | ||||
| -rw-r--r-- | Source/Dafny/Parser.ssc | 4 |
2 files changed, 9 insertions, 1 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index aff1deb7..9d232294 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -1076,7 +1076,11 @@ SelectOrCallSuffix<ref Expression! e> Expression<out ee> (. e1 = ee; .)
]
| ".." Expression<out ee> (. anyDots = true; e1 = ee; .)
- ) (. assert !anyDots ==> e0 != null;
+ ) (. if (!anyDots && e0 == null) {
+ /* a parsing error occurred */
+ e0 = dummyExpr;
+ }
+ assert !anyDots ==> e0 != null;
if (anyDots) {
assert e0 != null || e1 != null;
e = new SeqSelectExpr(x, false, e, e0, e1);
diff --git a/Source/Dafny/Parser.ssc b/Source/Dafny/Parser.ssc index ee979045..7b28ec2c 100644 --- a/Source/Dafny/Parser.ssc +++ b/Source/Dafny/Parser.ssc @@ -1698,6 +1698,10 @@ List<Expression!>! decreases) { Expression(out ee);
anyDots = true; e1 = ee;
} else Error(133);
+ if (!anyDots && e0 == null) {
+ /* a parsing error occurred */
+ e0 = dummyExpr;
+ }
assert !anyDots ==> e0 != null;
if (anyDots) {
assert e0 != null || e1 != null;
|