summaryrefslogtreecommitdiff
path: root/Test/dafny0
diff options
context:
space:
mode:
Diffstat (limited to 'Test/dafny0')
-rw-r--r--Test/dafny0/Answer29
-rw-r--r--Test/dafny0/Iterators.dfy49
2 files changed, 77 insertions, 1 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index 4de9e965..671c7c91 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1643,6 +1643,24 @@ Iterators.dfy(174,28): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon15_Then
+Iterators.dfy(205,7): Error: an assignment to _new is only allowed to shrink the set
+Execution trace:
+ (0,0): anon0
+ Iterators.dfy(194,3): anon17_LoopHead
+ (0,0): anon17_LoopBody
+ Iterators.dfy(194,3): anon18_Else
+ (0,0): anon5
+ Iterators.dfy(194,3): anon20_Else
+ (0,0): anon21_Then
+Iterators.dfy(209,21): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ Iterators.dfy(194,3): anon17_LoopHead
+ (0,0): anon17_LoopBody
+ Iterators.dfy(194,3): anon18_Else
+ (0,0): anon5
+ Iterators.dfy(194,3): anon20_Else
+ (0,0): anon22_Then
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:
@@ -1669,8 +1687,17 @@ Execution trace:
(0,0): anon0
(0,0): anon4_Then
(0,0): anon3
+Iterators.dfy(231,14): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ Iterators.dfy(222,3): anon15_LoopHead
+ (0,0): anon15_LoopBody
+ Iterators.dfy(222,3): anon16_Else
+ (0,0): anon8
+ Iterators.dfy(222,3): anon19_Else
+ (0,0): anon20_Else
-Dafny program verifier finished with 34 verified, 8 errors
+Dafny program verifier finished with 38 verified, 11 errors
-------------------- Superposition.dfy --------------------
diff --git a/Test/dafny0/Iterators.dfy b/Test/dafny0/Iterators.dfy
index 2473daa0..c6a0488b 100644
--- a/Test/dafny0/Iterators.dfy
+++ b/Test/dafny0/Iterators.dfy
@@ -184,3 +184,52 @@ static method AnotherMethod() returns (u: Cell, v: Cell)
{
u := new Cell;
}
+
+iterator DoleOutReferences(u: Cell) yields (r: Cell, c: Cell)
+ yield ensures r != null && fresh(r) && r !in _new;
+ yield ensures c != null && fresh(c); // but we don't say whether it's in _new
+ ensures false; // goes forever
+{
+ var myCells: seq<Cell> := [];
+ while (true)
+ invariant forall z :: z in myCells ==> z in _new;
+ {
+ c := new Cell;
+ r := new Cell;
+ c.data, r.data := 12, 12;
+ myCells := myCells + [c];
+ _new := _new - {r}; // remove our interest in 'r'
+ yield;
+ if (*) {
+ _new := _new + {c}; // fine, since 'c' is already in _new
+ _new := _new + {u}; // error: this does not shrink the set
+ } else if (*) {
+ assert c.data == 12; // still true, since 'c' is in _new
+ assert c in _new; // as is checked here as well
+ assert r.data == 12; // error: it may have changed
+ } else {
+ parallel (z | z in myCells) {
+ z.data := z.data + 1; // we're allowed to modify these, because they are all in _new
+ }
+ }
+ }
+}
+
+method ClientOfNewReferences()
+{
+ var m := new DoleOutReferences.DoleOutReferences(null);
+ var i := 86;
+ while (i != 0)
+ invariant m.Valid() && fresh(m._new);
+ {
+ var more := m.MoveNext();
+ assert more; // follows from 'ensures' clause of the iterator
+ if (*) {
+ m.r.data := i; // this change is allowed, because we own it
+ } else {
+ m.c.data := i; // this change, by itself, is allowed
+ assert m.Valid(); // error: ... however, don't expect m.Valid() to survive the change to m.c.data
+ }
+ i := i - 1;
+ }
+}