diff options
| author |  Rustan Leino <unknown> | 2015-06-15 17:00:04 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2015-06-15 17:00:04 -0700 |
| commit | cc0a7cae53c068993e3b3004049629dd396cb649 (patch) | |
| tree | bb1ae056cded89fdcddcd84294d6accc4c9d03ac /Test/dafny0/Reads.dfy.expect | |
| parent | 58d639bff25a2d4dadf6febb81b1438e957c43cd (diff) | |
Changed logical order of requires and reads clauses on functions. Reads clauses
can now assume the precondition (as had also been the case back in the days when
reads clauses had to be self framing).
Diffstat (limited to 'Test/dafny0/Reads.dfy.expect')
| -rw-r--r-- | Test/dafny0/Reads.dfy.expect | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/Test/dafny0/Reads.dfy.expect b/Test/dafny0/Reads.dfy.expect index 0b599f3f..1199797f 100644 --- a/Test/dafny0/Reads.dfy.expect +++ b/Test/dafny0/Reads.dfy.expect @@ -1,4 +1,4 @@ -Reads.dfy(79,11): Error: insufficient reads clause to read field
+Reads.dfy(133,11): Error: insufficient reads clause to read field
Execution trace:
(0,0): anon0
Reads.dfy(9,30): Error: insufficient reads clause to read field
@@ -7,8 +7,6 @@ Execution trace: Reads.dfy(18,30): Error: insufficient reads clause to read field
Execution trace:
(0,0): anon0
- (0,0): anon10_Then
- (0,0): anon4
Reads.dfy(28,50): Error: insufficient reads clause to read field
Execution trace:
(0,0): anon0
@@ -32,4 +30,4 @@ Reads.dfy(120,38): Error: insufficient reads clause to invoke function Execution trace:
(0,0): anon0
-Dafny program verifier finished with 16 verified, 9 errors
+Dafny program verifier finished with 17 verified, 9 errors
|