diff options
| author |  Jason Koenig <unknown> | 2012-07-16 15:12:43 -0700 |
|---|---|---|
| committer | Jason Koenig <unknown> | 2012-07-16 15:12:43 -0700 |
| commit | 7c5b29cfb26c4fe04de732ae7f79d12d840c679e (patch) | |
| tree | 781f09219ef8a47c88c827f14314ca0472feb144 /Source/Dafny/Dafny.atg | |
| parent | b9dfc55284aa0dcffcaf9c5ddbde51a77572b31a (diff) | |
Dafny: allow implict self (as in "`field") in frame declarations.
Diffstat (limited to 'Source/Dafny/Dafny.atg')
| -rw-r--r-- | Source/Dafny/Dafny.atg | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 54b9b4a4..5efbd57b 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -701,10 +701,14 @@ PossiblyWildFrameExpression<out FrameExpression/*!*/ fe> .
FrameExpression<out FrameExpression/*!*/ fe>
= (. Contract.Ensures(Contract.ValueAtReturn(out fe) != null); Expression/*!*/ e; IToken/*!*/ id; string fieldName = null; .)
- Expression<out e>
- [ "`" Ident<out id> (. fieldName = id.val; .)
- ]
- (. fe = new FrameExpression(e, fieldName); .)
+ (( Expression<out e>
+ [ "`" Ident<out id> (. fieldName = id.val; .)
+ ]
+ (. fe = new FrameExpression(e, fieldName); .)
+ ) |
+ ( "`" Ident<out id> (. fieldName = id.val; .)
+ (. fe = new FrameExpression(new ImplicitThisExpr(id), fieldName); .)
+ ))
.
FunctionBody<out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd>
= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); e = dummyExpr; .)
|