Project

General

Profile

Feature #9583

Update CPAchecker

Added by Evgeny Novikov 19 days ago. Updated 3 days ago.

Status:
New
Priority:
Urgent
Category:
Addons
Target version:
Start date:
04/03/2019
Due date:
% Done:

0%

Estimated time:
Published in build:

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.


Related issues

Blocked by Klever - Feature #9609: Avoid recursion in simple testsResolved04/19/2019

Actions

History

#1

Updated by Pavel Andrianov 16 days 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.

#2

Updated by Evgeny Novikov 16 days 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.

#3

Updated by Evgeny Novikov 4 days ago

https://gitlab.com/sosy-lab/software/cpachecker/issues/571 seems to be fixed. Let's try to switch to r31020.

#4

Updated by Evgeny Novikov 4 days 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.

#6

Updated by Evgeny Novikov 3 days ago

  • Blocked by Feature #9609: Avoid recursion in simple tests added
#7

Updated by Evgeny Novikov 3 days 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.

Also available in: Atom PDF