diff options
| author |  Rustan Leino <unknown> | 2015-06-15 14:42:44 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2015-06-15 14:42:44 -0700 |
| commit | b732961c4e4f174a184c34749d694e289d1e4f25 (patch) | |
| tree | 9b9ff9890a2ad1c9ac8a33aae67cbedfb0f8bfbd /Test/dafny0/Reads.dfy.expect | |
| parent | 9a105ad12e6487725a90a6401478bd9ab8b905b0 (diff) | |
More tests of reads-clause checking
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
|