Some more reads tests

2 files changed, 28 insertions, 1 deletions

diff --git a/Test/dafny0/Reads.dfy b/Test/dafny0/Reads.dfy
index 23064f54..f1c840c3 100644
--- a/Test/dafny0/Reads.dfy
+++ b/Test/dafny0/Reads.dfy
@@ -112,3 +112,17 @@ function ApplyToSet_AltSignature1<X>(S: set<X>, f: X -> X): set<X>
 function ApplyToSet_AltSignature2<X>(S: set<X>, f: X -> X): set<X>
   requires (forall x :: x in S ==> f.reads(x) == {}) ==> forall x :: x in S ==> f.requires(x)
   // (this precondition would not be good enough to check the body above)
+
+function FunctionInQuantifier0(): int
+  requires exists f: int -> int :: f(10) == 100  // error (x2): precondition violation and insufficient reads
+
+function FunctionInQuantifier1(): int
+  requires exists f: int -> int :: f.requires(10) && f(10) == 100  // error: insufficient reads
+
+function FunctionInQuantifier2(): int
+  requires exists f: int -> int :: f.reads(10) == {} && f.requires(10) && f(10) == 100
+  ensures FunctionInQuantifier2() == 100
+{
+  var f: int -> int :| f.reads(10) == {} && f.requires(10) && f(10) == 100;  // error: insufficient reads for f.reads(10)
+  f(10)
+}
diff --git a/Test/dafny0/Reads.dfy.expect b/Test/dafny0/Reads.dfy.expect
index 4dd1e947..79d290da 100644
--- a/Test/dafny0/Reads.dfy.expect
+++ b/Test/dafny0/Reads.dfy.expect
@@ -22,5 +22,18 @@ Execution trace:
     (0,0): anon0

     (0,0): anon10_Then

     (0,0): anon4

+Reads.dfy(117,36): Error: insufficient reads clause to invoke function

+Execution trace:

+    (0,0): anon0

+Reads.dfy(117,36): Error: possible violation of function precondition

+Execution trace:

+    (0,0): anon0

+Reads.dfy(120,38): Error: insufficient reads clause to invoke function

+Execution trace:

+    (0,0): anon0

+Reads.dfy(126,26): Error: insufficient reads clause to invoke function

+Execution trace:

+    (0,0): anon0

+    (0,0): anon8_Else

 

-Dafny program verifier finished with 15 verified, 6 errors

+Dafny program verifier finished with 15 verified, 10 errors