summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/Dafny/Dafny.atg7
-rw-r--r--Source/Dafny/Parser.cs11
-rw-r--r--Source/Dafny/Printer.cs18
-rw-r--r--Source/Dafny/Translator.cs1
-rw-r--r--Test/dafny0/Answer56
-rw-r--r--Test/dafny0/SmallTests.dfy12
6 files changed, 68 insertions, 37 deletions
diff --git a/Source/Dafny/Dafny.atg b/Source/Dafny/Dafny.atg
index 2f5228d9..c7eaa427 100644
--- a/Source/Dafny/Dafny.atg
+++ b/Source/Dafny/Dafny.atg
@@ -1090,13 +1090,16 @@ VarDeclStatement<.out Statement/*!*/ s.>
List<AssignmentRhs> rhss = new List<AssignmentRhs>();
IToken suchThatAssume = null;
Expression suchThat = null;
+ Attributes attrs = null;
.)
[ "ghost" (. isGhost = true; x = t; .)
]
"var" (. if (!isGhost) { x = t; } .)
- LocalIdentTypeOptional<out d, isGhost> (. lhss.Add(d); .)
+ { Attribute<ref attrs> }
+ LocalIdentTypeOptional<out d, isGhost> (. lhss.Add(d); d.Attributes = attrs; attrs = null; .)
{ ","
- LocalIdentTypeOptional<out d, isGhost> (. lhss.Add(d); .)
+ { Attribute<ref attrs> }
+ LocalIdentTypeOptional<out d, isGhost> (. lhss.Add(d); d.Attributes = attrs; attrs = null; .)
}
[ ":=" (. assignTok = t;
lhs0 = new IdentifierExpr(lhss[0].Tok, lhss[0].Name);
diff --git a/Source/Dafny/Parser.cs b/Source/Dafny/Parser.cs
index 05bf7e0d..6cfe852d 100644
--- a/Source/Dafny/Parser.cs
+++ b/Source/Dafny/Parser.cs
@@ -1698,6 +1698,7 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
List<AssignmentRhs> rhss = new List<AssignmentRhs>();
IToken suchThatAssume = null;
Expression suchThat = null;
+ Attributes attrs = null;
if (la.kind == 23) {
Get();
@@ -1705,12 +1706,18 @@ List<Expression/*!*/>/*!*/ decreases, ref Attributes decAttrs, ref Attributes mo
}
Expect(28);
if (!isGhost) { x = t; }
+ while (la.kind == 8) {
+ Attribute(ref attrs);
+ }
LocalIdentTypeOptional(out d, isGhost);
- lhss.Add(d);
+ lhss.Add(d); d.Attributes = attrs; attrs = null;
while (la.kind == 29) {
Get();
+ while (la.kind == 8) {
+ Attribute(ref attrs);
+ }
LocalIdentTypeOptional(out d, isGhost);
- lhss.Add(d);
+ lhss.Add(d); d.Attributes = attrs; attrs = null;
}
if (la.kind == 66 || la.kind == 68) {
if (la.kind == 66) {
diff --git a/Source/Dafny/Printer.cs b/Source/Dafny/Printer.cs
index 767d24b8..868d73f5 100644
--- a/Source/Dafny/Printer.cs
+++ b/Source/Dafny/Printer.cs
@@ -578,7 +578,12 @@ namespace Microsoft.Dafny {
if (s.IsGhost) {
wr.Write("ghost ");
}
- wr.Write("var {0}", s.DisplayName);
+ wr.Write("var");
+ if (s.HasAttributes())
+ {
+ PrintAttributes(s.Attributes);
+ }
+ wr.Write(" {0}", s.DisplayName);
PrintType(": ", s.OptionalType);
wr.Write(";");
@@ -732,12 +737,17 @@ namespace Microsoft.Dafny {
if (s.Lhss[0].IsGhost) {
wr.Write("ghost ");
}
- wr.Write("var ");
+ wr.Write("var");
string sep = "";
foreach (var lhs in s.Lhss) {
- wr.Write("{0}{1}", sep, lhs.DisplayName);
+ wr.Write(sep);
+ if (lhs.HasAttributes())
+ {
+ PrintAttributes(lhs.Attributes);
+ }
+ wr.Write(" {0}", lhs.DisplayName);
PrintType(": ", lhs.OptionalType);
- sep = ", ";
+ sep = ",";
}
if (s.Update != null) {
PrintUpdateRHS(s.Update);
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs
index ee7da643..16cabc1e 100644
--- a/Source/Dafny/Translator.cs
+++ b/Source/Dafny/Translator.cs
@@ -5299,6 +5299,7 @@ namespace Microsoft.Dafny {
Bpl.Type varType = TrType(s.Type);
Bpl.Expr wh = GetWhereClause(stmt.Tok, new Bpl.IdentifierExpr(stmt.Tok, s.AssignUniqueName(currentDeclaration), varType), s.Type, etran);
Bpl.LocalVariable var = new Bpl.LocalVariable(stmt.Tok, new Bpl.TypedIdent(stmt.Tok, s.AssignUniqueName(currentDeclaration), varType, wh));
+ var.Attributes = etran.TrAttributes(s.Attributes, null);;
locals.Add(var);
} else if (stmt is CallStmt) {
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 4feaf762..3bee3088 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -2087,14 +2087,14 @@ SmallTests.dfy(375,6): Error: cannot prove termination; try supplying a decrease
Execution trace:
(0,0): anon0
(0,0): anon3_Else
-SmallTests.dfy(669,14): Error: assertion violation
+SmallTests.dfy(679,14): Error: assertion violation
Execution trace:
(0,0): anon0
- SmallTests.dfy(666,5): anon7_LoopHead
+ SmallTests.dfy(676,5): anon7_LoopHead
(0,0): anon7_LoopBody
- SmallTests.dfy(666,5): anon8_Else
+ SmallTests.dfy(676,5): anon8_Else
(0,0): anon9_Then
-SmallTests.dfy(690,14): Error: assertion violation
+SmallTests.dfy(700,14): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon7_Then
@@ -2127,12 +2127,12 @@ SmallTests.dfy(390,41): Related location: This is the postcondition that might n
Execution trace:
(0,0): anon0
(0,0): anon6_Else
-SmallTests.dfy(540,12): Error: assertion violation
+SmallTests.dfy(550,12): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon3_Then
(0,0): anon2
-SmallTests.dfy(554,20): Error: left-hand sides 0 and 1 may refer to the same location
+SmallTests.dfy(564,20): Error: left-hand sides 0 and 1 may refer to the same location
Execution trace:
(0,0): anon0
(0,0): anon27_Then
@@ -2144,11 +2144,11 @@ Execution trace:
(0,0): anon31_Then
(0,0): anon32_Then
(0,0): anon12
-SmallTests.dfy(556,15): Error: left-hand sides 1 and 2 may refer to the same location
+SmallTests.dfy(566,15): Error: left-hand sides 1 and 2 may refer to the same location
Execution trace:
(0,0): anon0
(0,0): anon27_Then
- SmallTests.dfy(549,18): anon28_Else
+ SmallTests.dfy(559,18): anon28_Else
(0,0): anon4
(0,0): anon29_Else
(0,0): anon7
@@ -2160,16 +2160,16 @@ Execution trace:
(0,0): anon37_Then
(0,0): anon22
(0,0): anon38_Then
-SmallTests.dfy(563,25): Error: target object may be null
+SmallTests.dfy(573,25): Error: target object may be null
Execution trace:
(0,0): anon0
-SmallTests.dfy(576,10): Error: assertion violation
+SmallTests.dfy(586,10): Error: assertion violation
Execution trace:
(0,0): anon0
-SmallTests.dfy(600,5): Error: cannot establish the existence of LHS values that satisfy the such-that predicate
+SmallTests.dfy(610,5): Error: cannot establish the existence of LHS values that satisfy the such-that predicate
Execution trace:
(0,0): anon0
-SmallTests.dfy(623,10): Error: assertion violation
+SmallTests.dfy(633,10): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon8_Then
@@ -2177,21 +2177,21 @@ Execution trace:
(0,0): anon4
(0,0): anon10_Then
(0,0): anon7
-SmallTests.dfy(637,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate
+SmallTests.dfy(647,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate
Execution trace:
(0,0): anon0
(0,0): anon5_Then
(0,0): anon6_Then
(0,0): anon3
-SmallTests.dfy(639,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate
+SmallTests.dfy(649,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate
Execution trace:
(0,0): anon0
(0,0): anon5_Else
-SmallTests.dfy(652,9): Error: cannot establish the existence of LHS values that satisfy the such-that predicate
+SmallTests.dfy(662,9): Error: cannot establish the existence of LHS values that satisfy the such-that predicate
Execution trace:
(0,0): anon0
-Dafny program verifier finished with 85 verified, 33 errors
+Dafny program verifier finished with 87 verified, 33 errors
out.tmp.dfy(33,11): Error: index out of range
Execution trace:
(0,0): anon0
@@ -2313,12 +2313,12 @@ out.tmp.dfy(499,41): Related location: This is the postcondition that might not
Execution trace:
(0,0): anon0
(0,0): anon6_Else
-out.tmp.dfy(536,12): Error: assertion violation
+out.tmp.dfy(544,12): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon3_Then
(0,0): anon2
-out.tmp.dfy(550,20): Error: left-hand sides 0 and 1 may refer to the same location
+out.tmp.dfy(558,20): Error: left-hand sides 0 and 1 may refer to the same location
Execution trace:
(0,0): anon0
(0,0): anon27_Then
@@ -2330,11 +2330,11 @@ Execution trace:
(0,0): anon31_Then
(0,0): anon32_Then
(0,0): anon12
-out.tmp.dfy(552,15): Error: left-hand sides 1 and 2 may refer to the same location
+out.tmp.dfy(560,15): Error: left-hand sides 1 and 2 may refer to the same location
Execution trace:
(0,0): anon0
(0,0): anon27_Then
- out.tmp.dfy(545,17): anon28_Else
+ out.tmp.dfy(553,17): anon28_Else
(0,0): anon4
(0,0): anon29_Else
(0,0): anon7
@@ -2346,16 +2346,16 @@ Execution trace:
(0,0): anon37_Then
(0,0): anon22
(0,0): anon38_Then
-out.tmp.dfy(559,25): Error: target object may be null
+out.tmp.dfy(567,25): Error: target object may be null
Execution trace:
(0,0): anon0
-out.tmp.dfy(572,10): Error: assertion violation
+out.tmp.dfy(580,10): Error: assertion violation
Execution trace:
(0,0): anon0
-out.tmp.dfy(598,5): Error: cannot establish the existence of LHS values that satisfy the such-that predicate
+out.tmp.dfy(606,5): Error: cannot establish the existence of LHS values that satisfy the such-that predicate
Execution trace:
(0,0): anon0
-out.tmp.dfy(617,10): Error: assertion violation
+out.tmp.dfy(625,10): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon8_Then
@@ -2363,21 +2363,21 @@ Execution trace:
(0,0): anon4
(0,0): anon10_Then
(0,0): anon7
-out.tmp.dfy(631,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate
+out.tmp.dfy(639,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate
Execution trace:
(0,0): anon0
(0,0): anon5_Then
(0,0): anon6_Then
(0,0): anon3
-out.tmp.dfy(633,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate
+out.tmp.dfy(641,10): Error: cannot establish the existence of LHS values that satisfy the such-that predicate
Execution trace:
(0,0): anon0
(0,0): anon5_Else
-out.tmp.dfy(647,9): Error: cannot establish the existence of LHS values that satisfy the such-that predicate
+out.tmp.dfy(655,9): Error: cannot establish the existence of LHS values that satisfy the such-that predicate
Execution trace:
(0,0): anon0
-Dafny program verifier finished with 85 verified, 33 errors
+Dafny program verifier finished with 87 verified, 33 errors
-------------------- LetExpr.dfy --------------------
LetExpr.dfy(5,12): Error: assertion violation
diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index 75a42200..b3107bcb 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -190,7 +190,7 @@ class AllocatedTests {
{
var n := new Node;
var t := S + {n};
-
+
if (*) {
assert !fresh(n); // error: n was not allocated in the initial state
} else {
@@ -498,6 +498,16 @@ class AttributeTests {
}
}
+// ----------------------- test attributes on variable declarations --------
+
+static method TestAttributesVarDecls()
+{
+ var {:foo} foo;
+ var {:bar} bar := 0;
+ var {:foo} {:bar} foobar := {};
+ var {:baz} baz, {:foobaz} foobaz := true, false;
+}
+
// ----------------------- Pretty printing of !(!expr) --------
static method TestNotNot()
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-07 06:14:15 +0000