Project

General

Profile

Feature #9583

Update CPAchecker

Added by Evgeny Novikov 5 months ago. Updated 4 months ago.

Status:
Closed
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 testsClosed04/19/2019

Actions

History

#1

Updated by Pavel Andrianov 5 months 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 5 months 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 months 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 months 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 4 months ago

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

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

#8

Updated by Evgeny Novikov 4 months ago

Almost 2 weeks have gone, but the bug was not fixed. So, let's accept the current state of CPAchecker.

#9

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

Also available in: Atom PDF