diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-08-18 14:30:44 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-08-18 14:30:44 -0700 |
| commit | 38d6bebc924b429e46afa9f14fcb834268e38fce (patch) | |
| tree | b11eebe57cc4cbd25cc22ab2cdacd24f4a120c9a /Test/dafny0/Answer | |
| parent | 3901e6e672eb3c85472aa2750084ac4aba63d710 (diff) | |
Dafny: fixed bug in looking at the arguments of the :induction attribute
Diffstat (limited to 'Test/dafny0/Answer')
| -rw-r--r-- | Test/dafny0/Answer | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 9a8c7541..3a650ce2 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -520,8 +520,20 @@ Execution trace: Array.dfy(128,6): Error: assignment may update an array element not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
+Array.dfy(153,1): Error BP5003: A postcondition might not hold on this return path.
+Array.dfy(152,11): Related location: This is the postcondition that might not hold.
+Execution trace:
+ (0,0): anon0
+Array.dfy(177,1): Error BP5003: A postcondition might not hold on this return path.
+Array.dfy(176,11): Related location: This is the postcondition that might not hold.
+Execution trace:
+ (0,0): anon0
+Array.dfy(183,1): Error BP5003: A postcondition might not hold on this return path.
+Array.dfy(182,11): Related location: This is the postcondition that might not hold.
+Execution trace:
+ (0,0): anon0
-Dafny program verifier finished with 21 verified, 10 errors
+Dafny program verifier finished with 30 verified, 13 errors
-------------------- MultiDimArray.dfy --------------------
MultiDimArray.dfy(53,21): Error: assertion violation
|