summaryrefslogtreecommitdiff
path: root/Test/dafny0/TailCalls.dfy.expect
blob: 7fc51902ebb76b44dbfd05d32df9193d7ed5afc7 (plain)
1
2
3
4
5
6
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