diff options
| -rw-r--r-- | Source/Dafny/Translator.cs | 18 | ||||
| -rw-r--r-- | Test/dafny0/Answer | 42 | ||||
| -rw-r--r-- | Test/dafny0/IteratorResolution.dfy | 30 | ||||
| -rw-r--r-- | Test/dafny0/Iterators.dfy | 15 |
4 files changed, 94 insertions, 11 deletions
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 70a24310..c3073733 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -1640,7 +1640,12 @@ namespace Microsoft.Dafny { Contract.Requires(predef != null);
// set up the information used to verify the method's modifies clause
- DefineFrame(iter.tok, iter.Modifies.Expressions, builder, localVariables, null);
+ var iteratorFrame = new List<FrameExpression>();
+ var th = new ThisExpr(iter.tok);
+ th.Type = Resolver.GetThisType(iter.tok, iter); // resolve here
+ iteratorFrame.Add(new FrameExpression(iter.tok, th, null));
+ iteratorFrame.AddRange(iter.Modifies.Expressions);
+ DefineFrame(iter.tok, iteratorFrame, builder, localVariables, null);
}
Bpl.Cmd CaptureState(IToken tok, string/*?*/ additionalInfo) {
@@ -4149,7 +4154,8 @@ namespace Microsoft.Dafny { if (RefinementToken.IsInherited(split.E.tok, currentModule)) {
// this postcondition was inherited into this module, so just ignore it
} else if (!split.IsFree) {
- builder.Add(AssertNS(split.E.tok, split.E, "possible violation of yield-ensures condition", stmt.Tok));
+ var yieldToken = new NestedToken(s.Tok, split.E.tok);
+ builder.Add(AssertNS(yieldToken, split.E, "possible violation of yield-ensures condition", stmt.Tok));
}
}
builder.Add(new Bpl.AssumeCmd(stmt.Tok, yeEtran.TrExpr(p.E)));
@@ -6387,7 +6393,13 @@ namespace Microsoft.Dafny { Contract.Requires(layerOffset + offset <= 1);
Contract.Ensures(Contract.Result<ExpressionTranslator>() != null);
- return new ExpressionTranslator(translator, predef, HeapExpr, This, applyLimited_CurrentFunction, layerOffset + offset, modifiesFrame);
+ var et = new ExpressionTranslator(translator, predef, HeapExpr, This, applyLimited_CurrentFunction, layerOffset + offset, modifiesFrame);
+ if (this.oldEtran != null) {
+ var etOld = new ExpressionTranslator(translator, predef, Old.HeapExpr, This, applyLimited_CurrentFunction, layerOffset + offset, modifiesFrame);
+ etOld.oldEtran = etOld;
+ et.oldEtran = etOld;
+ }
+ return et;
}
public Bpl.IdentifierExpr TheFrame(IToken tok)
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 358a64bf..df0451d5 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1623,18 +1623,50 @@ IteratorResolution.dfy(79,13): Error: when allocating an object of type 'Generic IteratorResolution.dfy(83,15): Error: logical negation expects a boolean argument (instead got int)
IteratorResolution.dfy(17,11): Error: LHS of assignment does not denote a mutable field
IteratorResolution.dfy(19,12): Error: LHS of assignment does not denote a mutable field
-7 resolution/type errors detected in IteratorResolution.dfy
+IteratorResolution.dfy(123,9): Error: unresolved identifier: _decreases3
+IteratorResolution.dfy(124,21): Error: arguments must have the same type (got int and ?)
+IteratorResolution.dfy(125,14): Error: LHS of assignment does not denote a mutable field
+IteratorResolution.dfy(132,9): Error: unresolved identifier: _decreases1
+IteratorResolution.dfy(137,9): Error: unresolved identifier: _decreases0
+12 resolution/type errors detected in IteratorResolution.dfy
-------------------- Iterators.dfy --------------------
-Iterators.dfy(36,14): Error BP5002: A precondition for this call might not hold.
+Iterators.dfy(100,22): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+Iterators.dfy(103,14): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon4_Then
+ (0,0): anon3
+Iterators.dfy(37,14): Error BP5002: A precondition for this call might not hold.
Iterators.dfy(1,10): Related location: This is the precondition that might not hold.
Execution trace:
(0,0): anon0
- (0,0): anon31_Then
+ (0,0): anon37_Then
+ (0,0): anon2
+ (0,0): anon38_Then
+ (0,0): anon5
+ (0,0): anon39_Then
+Iterators.dfy(86,14): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+Iterators.dfy(116,16): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon3_Else
+Iterators.dfy(147,16): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon4_Else
+Iterators.dfy(152,16): Error BP5002: A precondition for this call might not hold.
+Iterators.dfy(122,10): Related location: This is the precondition that might not hold.
+Execution trace:
+ (0,0): anon0
+ (0,0): anon4_Then
(0,0): anon3
- (0,0): anon32_Then
-Dafny program verifier finished with 16 verified, 1 error
+Dafny program verifier finished with 27 verified, 7 errors
-------------------- Superposition.dfy --------------------
diff --git a/Test/dafny0/IteratorResolution.dfy b/Test/dafny0/IteratorResolution.dfy index 64d1ebd3..60b1bc7e 100644 --- a/Test/dafny0/IteratorResolution.dfy +++ b/Test/dafny0/IteratorResolution.dfy @@ -106,3 +106,33 @@ module Mx { }
}
}
+
+// --------------------------------- _decreases<n> fields
+
+class Cell
+{
+ var data: int;
+}
+
+iterator Dieter0(c: Cell)
+ requires c != null;
+ decreases c.data, c.data, c != null;
+{
+ assert _decreases0 == _decreases1;
+ assert _decreases2;
+ assert _decreases3 == null; // error: there is no _decreases3
+ assert _decreases0 == null; // error: type mismatch
+ _decreases2 := false; // error: the field is immutable
+}
+
+iterator Dieter1(c: Cell)
+ requires c != null;
+{
+ assert _decreases0 == c;
+ assert _decreases1; // error: there is no _decreases1
+}
+
+iterator Dieter2()
+{
+ assert _decreases0 == null; // error: there is no _decreases0
+}
diff --git a/Test/dafny0/Iterators.dfy b/Test/dafny0/Iterators.dfy index 36ba94cb..e1461622 100644 --- a/Test/dafny0/Iterators.dfy +++ b/Test/dafny0/Iterators.dfy @@ -93,9 +93,14 @@ iterator IterB(c: Cell) modifies c;
yield ensures c.data == old(c.data);
ensures true;
+ decreases c, c != null, c.data;
{
+ assert _decreases0 == c;
+ assert _decreases1 == (c != null);
+ assert _decreases2 == c.data; // error: c is not protected by the reads clause
+ var tmp := c.data;
if (*) { yield; }
- if (*) { yield; } // error: cannot prove the yield-ensures clause here (needs a reads clause)
+ assert tmp == c.data; // error: c is not protected by the reads clause
c.data := *;
}
@@ -120,9 +125,13 @@ iterator IterC(c: Cell) reads c;
yield ensures c.data == old(c.data);
ensures true;
+ decreases c, c, c.data;
{
- if (*) { yield; } // this time, all is fine, because the iterator has an appropriate reads clause
- if (*) { yield; } // this time, all is fine, because the iterator has an appropriate reads clause
+ assert _decreases2 == c.data; // this time, all is fine, because the iterator has an appropriate reads clause
+ var tmp := c.data;
+ if (*) { yield; }
+ if (*) { yield; }
+ assert tmp == c.data; // this time, all is fine, because the iterator has an appropriate reads clause
c.data := *;
}
|