diff options
| -rw-r--r-- | Test/dafny0/Reads.dfy | 14 | ||||
| -rw-r--r-- | Test/dafny0/Reads.dfy.expect | 15 |
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
|