diff options
author | 2012-06-13 19:02:21 -0700 | |
---|---|---|
committer | 2012-06-13 19:02:21 -0700 | |
commit | 998d686fdb6b31d25ef2b9f995f64a0187a154c9 (patch) | |
tree | 44097d73b01d71f16e2174c4c7fc0c52adf34fd9 /Source/Dafny/Dafny.atg | |
parent | 84219c03a73e14a7b0a74c4e94b38b8855f13fa7 (diff) | |
parent | de2e6cad0c25388aca044d42ad3cbd1a873f7637 (diff) |
Merge
Diffstat (limited to 'Source/Dafny/Dafny.atg')
-rw-r--r-- | Source/Dafny/Dafny.atg | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 0011c665..4a99c9ee 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -725,6 +725,7 @@ UpdateStmt<out Statement/*!*/ s> Expression lhs0;
IToken x;
Attributes attrs = null;
+ IToken suchThatAssume = null;
Expression suchThat = null;
.)
Lhs<out e> (. x = e.tok; .)
@@ -738,13 +739,15 @@ UpdateStmt<out Statement/*!*/ s> { "," Rhs<out r, lhs0> (. rhss.Add(r); .)
}
| ":|" (. x = t; .)
+ [ "assume" (. suchThatAssume = t; .)
+ ]
Expression<out suchThat>
)
";"
| ":" (. SemErr(t, "invalid statement (did you forget the 'label' keyword?)"); .)
)
(. if (suchThat != null) {
- s = new AssignSuchThatStmt(x, lhss, suchThat);
+ s = new AssignSuchThatStmt(x, lhss, suchThat, suchThatAssume);
} else {
s = new UpdateStmt(x, lhss, rhss);
}
@@ -807,6 +810,7 @@ VarDeclStatement<.out Statement/*!*/ s.> AssignmentRhs r; IdentifierExpr lhs0;
List<VarDecl> lhss = new List<VarDecl>();
List<AssignmentRhs> rhss = new List<AssignmentRhs>();
+ IToken suchThatAssume = null;
Expression suchThat = null;
.)
[ "ghost" (. isGhost = true; x = t; .)
@@ -824,6 +828,8 @@ VarDeclStatement<.out Statement/*!*/ s.> { "," Rhs<out r, lhs0> (. rhss.Add(r); .)
}
| ":|" (. assignTok = t; .)
+ [ "assume" (. suchThatAssume = t; .)
+ ]
Expression<out suchThat>
]
";"
@@ -833,7 +839,7 @@ VarDeclStatement<.out Statement/*!*/ s.> foreach (var lhs in lhss) {
ies.Add(new IdentifierExpr(lhs.Tok, lhs.Name));
}
- update = new AssignSuchThatStmt(assignTok, ies, suchThat);
+ update = new AssignSuchThatStmt(assignTok, ies, suchThat, suchThatAssume);
} else if (rhss.Count == 0) {
update = null;
} else {
|