diff options
Diffstat (limited to 'Source/Dafny/Dafny.atg')
| -rw-r--r-- | Source/Dafny/Dafny.atg | 19 |
1 files changed, 12 insertions, 7 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index d8d95079..1629fe51 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -18,7 +18,7 @@ static ModuleDecl theModule; static BuiltIns theBuiltIns;
static Expression/*!*/ dummyExpr = new LiteralExpr(Token.NoToken);
static AssignmentRhs/*!*/ dummyRhs = new ExprRhs(dummyExpr, null);
-static FrameExpression/*!*/ dummyFrameExpr = new FrameExpression(dummyExpr, null);
+static FrameExpression/*!*/ dummyFrameExpr = new FrameExpression(dummyExpr.tok, dummyExpr, null);
static Statement/*!*/ dummyStmt = new ReturnStmt(Token.NoToken, null);
static Attributes.Argument/*!*/ dummyAttrArg = new Attributes.Argument(Token.NoToken, "dummyAttrArg");
static int anonymousIds = 0;
@@ -703,19 +703,24 @@ PossiblyWildFrameExpression<out FrameExpression/*!*/ fe> * any use of the function. Nevertheless, as an experimental feature, the
* language allows it (and it is sound).
*/
- ( "*" (. fe = new FrameExpression(new WildcardExpr(t), null); .)
+ ( "*" (. fe = new FrameExpression(t, new WildcardExpr(t), null); .)
| FrameExpression<out fe>
)
.
FrameExpression<out FrameExpression/*!*/ fe>
-= (. Contract.Ensures(Contract.ValueAtReturn(out fe) != null); Expression/*!*/ e; IToken/*!*/ id; string fieldName = null; fe = null; .)
- (( Expression<out e>
- [ "`" Ident<out id> (. fieldName = id.val; .)
+= (. Contract.Ensures(Contract.ValueAtReturn(out fe) != null);
+ Expression/*!*/ e;
+ IToken/*!*/ id;
+ string fieldName = null; IToken feTok = null;
+ fe = null;
+ .)
+ (( Expression<out e> (. feTok = e.tok; .)
+ [ "`" Ident<out id> (. fieldName = id.val; feTok = id; .)
]
- (. fe = new FrameExpression(e, fieldName); .)
+ (. fe = new FrameExpression(feTok, e, fieldName); .)
) |
( "`" Ident<out id> (. fieldName = id.val; .)
- (. fe = new FrameExpression(new ImplicitThisExpr(id), fieldName); .)
+ (. fe = new FrameExpression(id, new ImplicitThisExpr(id), fieldName); .)
))
.
FunctionBody<out Expression/*!*/ e, out IToken bodyStart, out IToken bodyEnd>
|