diff options
Diffstat (limited to 'Source/Dafny/Dafny.atg')
| -rw-r--r-- | Source/Dafny/Dafny.atg | 18 |
1 files changed, 12 insertions, 6 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 071dbd64..e117ad67 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -843,6 +843,7 @@ WhileStmt<out Statement/*!*/ stmt> Expression guard;
List<MaybeFreeExpression/*!*/> invariants = new List<MaybeFreeExpression/*!*/>();
List<Expression/*!*/> decreases = new List<Expression/*!*/>();
+ List<FrameExpression/*!*/> mod = new List<FrameExpression/*!*/>();
Statement/*!*/ body;
IToken bodyStart, bodyEnd;
List<GuardedAlternative> alternatives;
@@ -851,20 +852,21 @@ WhileStmt<out Statement/*!*/ stmt> "while" (. x = t; .)
(
Guard<out guard> (. Contract.Assume(guard == null || cce.Owner.None(guard)); .)
- LoopSpec<out invariants, out decreases>
+ LoopSpec<out invariants, out decreases, out mod>
BlockStmt<out body, out bodyStart, out bodyEnd>
- (. stmt = new WhileStmt(x, guard, invariants, decreases, body); .)
+ (. stmt = new WhileStmt(x, guard, invariants, decreases, mod, body); .)
|
- LoopSpec<out invariants, out decreases>
+ LoopSpec<out invariants, out decreases, out mod>
AlternativeBlock<out alternatives>
- (. stmt = new AlternativeLoopStmt(x, invariants, decreases, alternatives); .)
+ (. stmt = new AlternativeLoopStmt(x, invariants, decreases, mod, alternatives); .)
)
.
-LoopSpec<.out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!*/> decreases.>
-= (. bool isFree; Expression/*!*/ e;
+LoopSpec<.out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!*/> decreases, out List<FrameExpression/*!*/> mod.>
+= (. bool isFree; Expression/*!*/ e; FrameExpression/*!*/ fe;
invariants = new List<MaybeFreeExpression/*!*/>();
decreases = new List<Expression/*!*/>();
+ mod = new List<FrameExpression/*!*/>();
.)
{ (. isFree = false; .)
[ "free" (. isFree = true; .)
@@ -873,6 +875,10 @@ LoopSpec<.out List<MaybeFreeExpression/*!*/> invariants, out List<Expression/*!* Expression<out e> (. invariants.Add(new MaybeFreeExpression(e, isFree)); .)
";"
| "decreases" DecreasesList<decreases, true> ";"
+ | "modifies" [ FrameExpression<out fe> (. mod.Add(fe); .)
+ { "," FrameExpression<out fe> (. mod.Add(fe); .)
+ }
+ ] ";"
}
.
|