diff options
| author |  leino <unknown> | 2015-06-12 13:01:36 -0700 |
|---|---|---|
| committer | leino <unknown> | 2015-06-12 13:01:36 -0700 |
| commit | 03a8bdfce9713570fdb3fcc05a31c6a83e26afd8 (patch) | |
| tree | 912ac184ec57c295b7feb17b75653c264821cc88 /Test/dafny0/Definedness.dfy.expect | |
| parent | 1e9a9af1700f67dde62e8ceb81aa16e13de0e3fb (diff) | |
Combined some common routines into CheckWellformedAndAssume, which also allows an improvement of the generated Boogie (which will be especially good soon, when reads-clause checking may change)
Diffstat (limited to 'Test/dafny0/Definedness.dfy.expect')
| -rw-r--r-- | Test/dafny0/Definedness.dfy.expect | 10 |
1 files changed, 3 insertions, 7 deletions
diff --git a/Test/dafny0/Definedness.dfy.expect b/Test/dafny0/Definedness.dfy.expect index 41073c0e..5d823616 100644 --- a/Test/dafny0/Definedness.dfy.expect +++ b/Test/dafny0/Definedness.dfy.expect @@ -161,19 +161,15 @@ Definedness.dfy(215,10): Error BP5003: A postcondition might not hold on this re Definedness.dfy(217,46): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
- (0,0): anon5_Else
+ (0,0): anon3_Else
Definedness.dfy(224,22): Error: target object may be null
Execution trace:
(0,0): anon0
- (0,0): anon5_Then
- (0,0): anon2
- (0,0): anon6_Then
+ (0,0): anon3_Then
Definedness.dfy(237,10): Error BP5003: A postcondition might not hold on this return path.
Definedness.dfy(240,24): Related location: This is the postcondition that might not hold.
Execution trace:
(0,0): anon0
- (0,0): anon7_Then
- (0,0): anon2
- (0,0): anon8_Else
+ (0,0): anon3_Else
Dafny program verifier finished with 21 verified, 37 errors
|