diff options
Diffstat (limited to 'Test/dafny0/TailCalls.dfy.expect')
| -rw-r--r-- | Test/dafny0/TailCalls.dfy.expect | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/Test/dafny0/TailCalls.dfy.expect b/Test/dafny0/TailCalls.dfy.expect index 7fc51902..dc1eec5b 100644 --- a/Test/dafny0/TailCalls.dfy.expect +++ b/Test/dafny0/TailCalls.dfy.expect @@ -1,6 +1,4 @@ TailCalls.dfy(21,15): Error: this recursive call is not recognized as being tail recursive, because it is followed by non-ghost code
-TailCalls.dfy(33,12): Error: 'decreases *' is allowed only on tail-recursive methods
-TailCalls.dfy(40,12): Error: 'decreases *' is allowed only on tail-recursive methods
-TailCalls.dfy(45,12): Error: 'decreases *' is allowed only on tail-recursive methods
-TailCalls.dfy(67,12): Error: 'decreases *' is allowed only on tail-recursive methods
-5 resolution/type errors detected in TailCalls.dfy
+TailCalls.dfy(38,24): Error: sorry, tail-call optimizations are not supported for mutually recursive methods
+TailCalls.dfy(43,24): Error: sorry, tail-call optimizations are not supported for mutually recursive methods
+3 resolution/type errors detected in TailCalls.dfy
|