Feature #9583
closedUpdate CPAchecker
0%
Description
Pavel reported that one of optimizations in CPAchecker was broken, so that the currently used version can spend too much time for verification for programs with recursion. We need to update to r30896.
BTW, Pavel says, that at the moment CPAchecker is more precise with recursion, so, if one will need such the precision, it will be necessary to change configuration (as far as I understand, get rid of option -skipRecursion).
With this update we will likely get a fix of https://gitlab.com/sosy-lab/software/cpachecker/issues/348.
It will be great to update after https://gitlab.com/sosy-lab/software/cpachecker/issues/571 will be investigated and fixed by somebody in our room.
Updated by Pavel Andrianov about 5 years ago
Just a note. If you get rid from -skipRecursion, CPAchecker fails after it detects a recursion. So, to handle recursive procedures you need a special version of BAM algorithm. We experimented with it long ago and it was very slow. If you are interested in it, we may check its status now.
Updated by Evgeny Novikov about 5 years ago
Pavel Andrianov wrote:
Just a note. If you get rid from -skipRecursion, CPAchecker fails after it detects a recursion. So, to handle recursive procedures you need a special version of BAM algorithm. We experimented with it long ago and it was very slow. If you are interested in it, we may check its status now.
Thank you for the additional note. I'm not interested much in support of recursion, so, let's experiment one day later.
Updated by Evgeny Novikov about 5 years ago
https://gitlab.com/sosy-lab/software/cpachecker/issues/571 seems to be fixed. Let's try to switch to r31020.
Updated by Evgeny Novikov about 5 years ago
I switched CPAchecker to r31020 in branch update-cpachecker. But tests demonstrated regressions. So, we have to wait for comments and likely for a new version of CPAchecker.
Updated by Evgeny Novikov about 5 years ago
Other two blocking issues are: https://gitlab.com/sosy-lab/software/cpachecker/issues/579 and https://gitlab.com/sosy-lab/software/cpachecker/issues/580.
Updated by Evgeny Novikov about 5 years ago
- Blocked by Feature #9609: Avoid recursion in simple tests added
Updated by Evgeny Novikov about 5 years ago
https://gitlab.com/sosy-lab/software/cpachecker/issues/580 was closed as irrelevant (before CPAchecker works a bit better with recursion, but that was a bug). We are looking forward for https://gitlab.com/sosy-lab/software/cpachecker/issues/579.
Updated by Evgeny Novikov almost 5 years ago
Almost 2 weeks have gone, but the bug was not fixed. So, let's accept the current state of CPAchecker.
Updated by Evgeny Novikov almost 5 years ago
- Status changed from New to Closed
Tests passed, so, I merged the branch to master in 1085dfa3c. Do not forget to re-build a build base for testing requirement specifications, populate updated configuration files and update existing ones.