More tests of reads-clause checking

2 files changed, 46 insertions, 1 deletions

diff --git a/Test/dafny0/Reads.dfy b/Test/dafny0/Reads.dfy
index 645494cb..6ae07d53 100644
--- a/Test/dafny0/Reads.dfy
+++ b/Test/dafny0/Reads.dfy
@@ -55,3 +55,39 @@ function ok5(r : R):()
   reads if r != null then {r, r.r} else {};
 {()}
 
+// Reads checking where there are circularities among the expressions
+
+class CircularChecking {
+  var Repr: set<object>
+    
+  function F(): int
+    reads this, Repr
+
+  function F'(): int
+    reads Repr, this  // this is also fine
+
+  function G0(): int
+    reads this
+    requires Repr == {} && F() == 100
+
+  function G1(): int
+    reads this
+    requires F() == 100  // error: it is not known (yet) that the rest of what F() reads (namely, Repr) is empty
+    requires Repr == {}
+
+  function H0(cell: Cell): int
+    reads Repr  // error: reads is not self-framing (unless "this in Repr")
+    requires this in Repr  // lo and behold!  So, reads clause is fine, if we can assume the precondition
+
+  function H1(cell: Cell): int
+    reads this, Repr
+    requires cell in Repr
+    requires cell != null && cell.data == 10
+
+  function H2(cell: Cell): int
+    reads this, Repr
+    requires cell != null && cell.data == 10  // error: it is not known (yet) that "cell in Repr"
+    requires cell in Repr
+}
+
+class Cell { var data: int }
diff --git a/Test/dafny0/Reads.dfy.expect b/Test/dafny0/Reads.dfy.expect
index 1cd17d16..0b6a2d5a 100644
--- a/Test/dafny0/Reads.dfy.expect
+++ b/Test/dafny0/Reads.dfy.expect
@@ -1,3 +1,12 @@
+Reads.dfy(75,14): Error: insufficient reads clause to invoke function

+Execution trace:

+    (0,0): anon0

+Reads.dfy(79,11): Error: insufficient reads clause to read field

+Execution trace:

+    (0,0): anon0

+Reads.dfy(89,35): Error: insufficient reads clause to read field

+Execution trace:

+    (0,0): anon0

 Reads.dfy(9,30): Error: insufficient reads clause to read field

 Execution trace:

     (0,0): anon0

@@ -19,4 +28,4 @@ Execution trace:
     (0,0): anon9_Then

     (0,0): anon3

 

-Dafny program verifier finished with 5 verified, 5 errors

+Dafny program verifier finished with 9 verified, 8 errors