diff options
Diffstat (limited to 'Source/Dafny/Dafny.atg')
| -rw-r--r-- | Source/Dafny/Dafny.atg | 22 |
1 files changed, 17 insertions, 5 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg index 3000d348..4b9e0c27 100644 --- a/Source/Dafny/Dafny.atg +++ b/Source/Dafny/Dafny.atg @@ -1036,11 +1036,11 @@ CaseStatement<out MatchCaseStmt/*!*/ c> /*------------------------------------------------------------------------*/
AssertStmt<out Statement/*!*/ s>
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;
- Expression/*!*/ e = null; Attributes attrs = null;
+ Expression e = null; Attributes attrs = null;
.)
- "assert" (. x = t; s = null;.)
+ "assert" (. x = t; .)
{ IF(IsAttribute()) Attribute<ref attrs> }
- ( Expression<out e>
+ ( Expression<out e>
| "..."
)
";"
@@ -1052,9 +1052,21 @@ AssertStmt<out Statement/*!*/ s> .)
.
AssumeStmt<out Statement/*!*/ s>
-= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Expression/*!*/ e; .)
+= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x;
+ Expression e = null; Attributes attrs = null;
+ .)
"assume" (. x = t; .)
- Expression<out e> ";" (. s = new AssumeStmt(x, e); .)
+ { IF(IsAttribute()) Attribute<ref attrs> }
+ ( Expression<out e>
+ | "..."
+ )
+ (. if (e == null) {
+ s = new SkeletonStatement(new AssumeStmt(x, new LiteralExpr(x, true), attrs), true, false);
+ } else {
+ s = new AssumeStmt(x, e, attrs);
+ }
+ .)
+ ";"
.
PrintStmt<out Statement/*!*/ s>
= (. Contract.Ensures(Contract.ValueAtReturn(out s) != null); IToken/*!*/ x; Attributes.Argument/*!*/ arg;
|