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/hofs/Classes.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/hofs/Classes.dfy.expect')
| -rw-r--r-- | Test/hofs/Classes.dfy.expect | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/Test/hofs/Classes.dfy.expect b/Test/hofs/Classes.dfy.expect index 21188d62..e490dbe0 100644 --- a/Test/hofs/Classes.dfy.expect +++ b/Test/hofs/Classes.dfy.expect @@ -1,10 +1,7 @@ -Classes.dfy(41,6): Error: possible violation of function precondition
+Classes.dfy(40,6): Error: possible violation of function precondition
Execution trace:
(0,0): anon0
- (0,0): anon13_Then
- (0,0): anon4
- (0,0): anon14_Then
- (0,0): anon15_Else
- (0,0): anon16_Else
+ (0,0): anon7_Else
+ (0,0): anon8_Else
Dafny program verifier finished with 6 verified, 1 error
|