Complex recursive function calls lead to false alarms in termination analysis
For complex recursive function calls (such as mutual or nested recursions), the termination analysis leads to false alarms when run using the
-terminationAnalysisWithRecursion
config.
This is currently not shown in the nightly-termination integration test, as the analysis there is executed without the recursion-extension, and is hence aborted early because of correctly recognizing the existence of recursive function calls.
This currently affects the following tasks:
- recursive-simple/fibo_5-1.c
- recursive-simple/fibo_5-2.c
- termination-crafted/NestedRecursion_1d.c
Command line:
scripts/cpa.sh -svcomp21 -spec test/programs/benchmarks/properties/termination.prp test/programs/benchmarks/recursive-simple/fibo_5-1.c
Below is a minimal code snippet shown for demonstration, which was taken from the NestedReucrsion_1d.c
task:
extern int __VERIFIER_nondet_int();
int rec1(int i) {
if(i <= 0)
return 0;
return rec1(rec1(rec1(i-2) - 1)) + 1;
}
int rec2(int j) {
if(j <= 0)
return 0;
return rec2(rec1(j)-1) - 1;
}
int main() {
int x = __VERIFIER_nondet_int();
rec2(x);
}