diff options
Diffstat (limited to 'Test/dafny0/Reads.dfy.expect')
| -rw-r--r-- | Test/dafny0/Reads.dfy.expect | 11 |
1 files changed, 10 insertions, 1 deletions
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
|