Casting in recursive function calls lead to false alarms in termination analysis
The are currently three recursion tasks that are evaluated wrongly by CPAchecker, which are as follows:
- recursive-simple/id_b3_o2-2.c
- recursive-simple/id_b3_o5-2.c
- recursive-simple/id_b5_o10-2.c
The tasks are all similar in structure and have the intention of testing the cast of an int
variable to an unsigned int
within recursive function calls.
An example is given below (a minimized example of recursive-simple/id_b3_o2-2.c
), which is guaranteed to eventually terminate, however, where CPAchecker comes up with a false alarm:
extern int __VERIFIER_nondet_int();
int id(int x) {
if (x==0)
return 0;
int ret = id((unsigned int)x-1) + 1;
if (ret > 3)
return 3;
return ret;
}
int main(void) {
int input = __VERIFIER_nondet_int();
id(input);
}
Edit: Adding a command line for reproduction:
scripts/cpa.sh -svcomp21 -spec test/programs/benchmarks/properties/termination.prp test/programs/benchmarks/recursive-simple/id_b3_o2-2.c
The config -svcomp21
can alternatively replaced by using the config -terminationAnalysisWithRecursion
Edited by Thomas Bunk