1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
|
CORE
main.c
--apply-loop-contracts
^\[ackermann\.\d+\] line 21 Check loop invariant before entry: SUCCESS$
^\[ackermann\.\d+\] line 21 Check that loop invariant is preserved: SUCCESS$
^\[ackermann\.\d+\] line 21 Check decreases clause on loop iteration: SUCCESS$
^\[ackermann.assigns.\d+\] line 29 Check that m is assignable: SUCCESS$
^\[ackermann.assigns.\d+\] line 30 Check that n is assignable: SUCCESS$
^\[ackermann.assigns.\d+\] line 35 Check that m is assignable: SUCCESS$
^\[ackermann.overflow.\d+] line 39 arithmetic overflow on signed \+ in n \+ 1: FAILURE$
^\*\* 1 of \d+ failed
^VERIFICATION FAILED$
^EXIT=10$
^SIGNAL=0$
--
--
It tests whether we can prove (only partially) the termination of the Ackermann
function using a multidimensional decreases clause.
Note that this particular implementation of the Ackermann function contains
both a while-loop and recursion. Therefore, to fully prove the termination of
the Ackermann function, we must prove both
(i) the termination of the while-loop and
(ii) the termination of the recursion.
Because CBMC does not support termination proofs of recursions (yet), we cannot
prove the latter, but the former. Hence, the termination proof in the code is
only "partial."
|
