diff options
| author |  chmaria <unknown> | 2014-11-01 13:59:31 +0100 |
|---|---|---|
| committer | chmaria <unknown> | 2014-11-01 13:59:31 +0100 |
| commit | 6e5fb70941531435489c1dc533d7caea9120a3d5 (patch) | |
| tree | 4b575de9ef5c17bdf61c805233adbdb2360d0f4c /Source/Dafny/Dafny.atg | |
| parent | 9f41b35b514eba87a037cbada83f0c294eafb936 (diff) | |
Added initial support for dirty while statements.
Diffstat (limited to 'Source/Dafny/Dafny.atg')
| -rw-r--r-- | Source/Dafny/Dafny.atg | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 18ac5e16..690f8403 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -1407,6 +1407,7 @@ WhileStmt<out Statement/*!*/ stmt> IToken bodyStart = null, bodyEnd = null, endTok = Token.NoToken;
List<GuardedAlternative> alternatives;
stmt = dummyStmt; // to please the compiler
+ bool isDirtyLoop = true;
.)
"while" (. x = t; .)
(
@@ -1419,22 +1420,24 @@ WhileStmt<out Statement/*!*/ stmt> | "..." (. guardEllipsis = t; .)
)
LoopSpec<out invariants, out decreases, out mod, ref decAttrs, ref modAttrs>
- ( BlockStmt<out body, out bodyStart, out bodyEnd> (. endTok = body.EndTok; .)
- | "..." (. bodyEllipsis = t; endTok = t; .)
- )
+ [ BlockStmt<out body, out bodyStart, out bodyEnd> (. endTok = body.EndTok; isDirtyLoop = false; .)
+ | "..." (. bodyEllipsis = t; endTok = t; isDirtyLoop = false; .)
+ ]
(.
if (guardEllipsis != null || bodyEllipsis != null) {
if (mod != null) {
SemErr(mod[0].E.tok, "'modifies' clauses are not allowed on refining loops");
}
- if (body == null) {
+ if (body == null && !isDirtyLoop) {
body = new BlockStmt(x, endTok, new List<Statement>());
}
stmt = new WhileStmt(x, endTok, guard, invariants, new Specification<Expression>(decreases, decAttrs), new Specification<FrameExpression>(null, null), body);
stmt = new SkeletonStatement(stmt, guardEllipsis, bodyEllipsis);
} else {
// The following statement protects against crashes in case of parsing errors
- body = body ?? new BlockStmt(x, endTok, new List<Statement>());
+ if (body == null && !isDirtyLoop) {
+ body = new BlockStmt(x, endTok, new List<Statement>());
+ }
stmt = new WhileStmt(x, endTok, guard, invariants, new Specification<Expression>(decreases, decAttrs), new Specification<FrameExpression>(mod, modAttrs), body);
}
.)
|