diff options
| author |  rustanleino <unknown> | 2010-05-18 04:43:55 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-05-18 04:43:55 +0000 |
| commit | 9657b7042a5a55fe96bc9b7560c473876d7efa60 (patch) | |
| tree | 04c1398e863725350adfef9a7740151354065843 /Source/Dafny | |
| parent | 71d821b322b391630be2cc8b610111d9f35cbd75 (diff) | |
Dafny: Fixed crash in parser (that occurred when the Dafny input had a particular parsing error).
Diffstat (limited to 'Source/Dafny')
| -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;
|