diff options
| -rw-r--r-- | Dafny/Dafny.atg | 11 | ||||
| -rw-r--r-- | Dafny/DafnyAst.cs | 6 | ||||
| -rw-r--r-- | Dafny/Parser.cs | 19 | ||||
| -rw-r--r-- | Dafny/Printer.cs | 11 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 2 | ||||
| -rw-r--r-- | Test/dafny0/SmallTests.dfy | 40 |
6 files changed, 79 insertions, 10 deletions
diff --git a/Dafny/Dafny.atg b/Dafny/Dafny.atg index 92888800..67347e2a 100644 --- a/Dafny/Dafny.atg +++ b/Dafny/Dafny.atg @@ -694,9 +694,11 @@ UpdateStmt<out Statement/*!*/ s> Expression e; AssignmentRhs r;
Expression lhs0;
IToken x;
+ Attributes attrs = null;
.)
Lhs<out e> (. x = e.tok; .)
- ( ";" (. rhss.Add(new ExprRhs(e)); .)
+ ( { IF(IsAttribute()) Attribute<ref attrs> }
+ ";" (. rhss.Add(new ExprRhs(e)); .)
| (. lhss.Add(e); lhs0 = e; .)
{ "," Lhs<out e> (. lhss.Add(e); .)
}
@@ -704,10 +706,11 @@ UpdateStmt<out Statement/*!*/ s> Rhs<out r, lhs0> (. rhss.Add(r); .)
{ "," Rhs<out r, lhs0> (. rhss.Add(r); .)
}
+ { IF(IsAttribute()) Attribute<ref attrs> }
";"
| ":" (. SemErr(t, "invalid statement (did you forget the 'label' keyword?)"); .)
)
- (. s = new UpdateStmt(x, lhss, rhss); .)
+ (. s = new UpdateStmt(x, lhss, rhss, attrs); .)
.
Rhs<out AssignmentRhs r, Expression receiverForInitCall>
= (. IToken/*!*/ x, newToken; Expression/*!*/ e;
@@ -749,6 +752,7 @@ VarDeclStatement<.out Statement/*!*/ s.> AssignmentRhs r; IdentifierExpr lhs0;
List<VarDecl> lhss = new List<VarDecl>();
List<AssignmentRhs> rhss = new List<AssignmentRhs>();
+ Attributes attrs = null;
.)
[ "ghost" (. isGhost = true; x = t; .)
]
@@ -764,6 +768,7 @@ VarDeclStatement<.out Statement/*!*/ s.> Rhs<out r, lhs0> (. rhss.Add(r); .)
{ "," Rhs<out r, lhs0> (. rhss.Add(r); .)
}
+ { IF(IsAttribute()) Attribute<ref attrs> }
]
";"
(. UpdateStmt update;
@@ -774,7 +779,7 @@ VarDeclStatement<.out Statement/*!*/ s.> foreach (var lhs in lhss) {
ies.Add(new AutoGhostIdentifierExpr(lhs.Tok, lhs.Name));
}
- update = new UpdateStmt(assignTok, ies, rhss);
+ update = new UpdateStmt(assignTok, ies, rhss, attrs);
}
s = new VarDeclStmt(x, lhss, update);
.)
diff --git a/Dafny/DafnyAst.cs b/Dafny/DafnyAst.cs index 92d97b38..1470c0b3 100644 --- a/Dafny/DafnyAst.cs +++ b/Dafny/DafnyAst.cs @@ -1567,7 +1567,7 @@ namespace Microsoft.Dafny { Contract.Invariant(cce.NonNullElements(Lhss));
Contract.Invariant(cce.NonNullElements(Rhss));
}
- public UpdateStmt(IToken tok, List<Expression> lhss, List<AssignmentRhs> rhss)
+ public UpdateStmt(IToken tok, List<Expression> lhss, List<AssignmentRhs> rhss, Attributes attrs = null)
: base(tok)
{
Contract.Requires(tok != null);
@@ -1577,8 +1577,9 @@ namespace Microsoft.Dafny { Lhss = lhss;
Rhss = rhss;
CanMutateKnownState = false;
+ Attributes = attrs;
}
- public UpdateStmt(IToken tok, List<Expression> lhss, List<AssignmentRhs> rhss, bool mutate)
+ public UpdateStmt(IToken tok, List<Expression> lhss, List<AssignmentRhs> rhss, bool mutate, Attributes attrs = null)
: base(tok)
{
Contract.Requires(tok != null);
@@ -1588,6 +1589,7 @@ namespace Microsoft.Dafny { Lhss = lhss;
Rhss = rhss;
CanMutateKnownState = mutate;
+ Attributes = attrs;
}
}
diff --git a/Dafny/Parser.cs b/Dafny/Parser.cs index d019b017..371bb2c8 100644 --- a/Dafny/Parser.cs +++ b/Dafny/Parser.cs @@ -1126,11 +1126,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Expression e; AssignmentRhs r;
Expression lhs0;
IToken x;
+ Attributes attrs = null;
Lhs(out e);
x = e.tok;
- if (la.kind == 18) {
- Get();
+ if (la.kind == 6 || la.kind == 18) {
+ while (IsAttribute()) {
+ Attribute(ref attrs);
+ }
+ Expect(18);
rhss.Add(new ExprRhs(e));
} else if (la.kind == 20 || la.kind == 50) {
lhss.Add(e); lhs0 = e;
@@ -1148,12 +1152,15 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Rhs(out r, lhs0);
rhss.Add(r);
}
+ while (IsAttribute()) {
+ Attribute(ref attrs);
+ }
Expect(18);
} else if (la.kind == 5) {
Get();
SemErr(t, "invalid statement (did you forget the 'label' keyword?)");
} else SynErr(136);
- s = new UpdateStmt(x, lhss, rhss);
+ s = new UpdateStmt(x, lhss, rhss, attrs);
}
void VarDeclStatement(out Statement/*!*/ s) {
@@ -1162,6 +1169,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo AssignmentRhs r; IdentifierExpr lhs0;
List<VarDecl> lhss = new List<VarDecl>();
List<AssignmentRhs> rhss = new List<AssignmentRhs>();
+ Attributes attrs = null;
if (la.kind == 12) {
Get();
@@ -1189,6 +1197,9 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo Rhs(out r, lhs0);
rhss.Add(r);
}
+ while (IsAttribute()) {
+ Attribute(ref attrs);
+ }
}
Expect(18);
UpdateStmt update;
@@ -1199,7 +1210,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo foreach (var lhs in lhss) {
ies.Add(new AutoGhostIdentifierExpr(lhs.Tok, lhs.Name));
}
- update = new UpdateStmt(assignTok, ies, rhss);
+ update = new UpdateStmt(assignTok, ies, rhss, attrs);
}
s = new VarDeclStmt(x, lhss, update);
diff --git a/Dafny/Printer.cs b/Dafny/Printer.cs index 8a321b90..7649fa11 100644 --- a/Dafny/Printer.cs +++ b/Dafny/Printer.cs @@ -640,6 +640,12 @@ namespace Microsoft.Dafny { PrintRhs(rhs);
sep = ", ";
}
+
+ if (stmt.HasAttributes())
+ {
+ PrintAttributes(stmt.Attributes);
+ }
+
wr.Write(";");
} else if (stmt is VarDeclStmt) {
@@ -662,6 +668,11 @@ namespace Microsoft.Dafny { PrintRhs(rhs);
sep = ", ";
}
+
+ if (s.Update.HasAttributes())
+ {
+ PrintAttributes(s.Update.Attributes);
+ }
}
wr.Write(";");
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index aa58ac6e..5e1428c2 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -247,7 +247,7 @@ SmallTests.dfy(411,41): Error: possible violation of function postcondition Execution trace:
(0,0): anon6_Else
-Dafny program verifier finished with 49 verified, 21 errors
+Dafny program verifier finished with 56 verified, 21 errors
-------------------- Definedness.dfy --------------------
Definedness.dfy(8,7): Error: possible division by zero
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy index 7adc26a3..e6590ed1 100644 --- a/Test/dafny0/SmallTests.dfy +++ b/Test/dafny0/SmallTests.dfy @@ -418,6 +418,26 @@ function F(b: bool): int class AttributeTests {
var f: int;
+ method m0()
+ {
+
+ }
+
+ method m1() returns (r: bool)
+ {
+ r := false;
+ }
+
+ function method m2() : bool
+ {
+ true
+ }
+
+ constructor C()
+ {
+
+ }
+
method testAttributes0()
ensures {:boolAttr true} true;
ensures {:boolAttr false} true;
@@ -465,5 +485,25 @@ class AttributeTests { {
}
+
+ m0() {:boolAttr true};
+ m0() {:boolAttr false};
+ m0() {:intAttr 0};
+ m0() {:intAttr 1};
+
+ var b1 := m1() {:boolAttr true};
+ b1 := m1() {:boolAttr false};
+ b1 := m1() {:intAttr 0};
+ b1 := m1() {:intAttr 1};
+
+ var b2 := m2() {:boolAttr true};
+ b2 := m2() {:boolAttr false};
+ b2 := m2() {:intAttr 0};
+ b2 := m2() {:intAttr 1};
+
+ var c := new AttributeTests.C() {:boolAttr true};
+ c := new AttributeTests.C() {:boolAttr false};
+ c := new AttributeTests.C() {:intAttr 0};
+ c := new AttributeTests.C() {:intAttr 1};
}
}
|