Feature #9532
closedBug #6629: Used CIL is outdated
Update CPAchecker
0%
Description
New versions of CPAchecker will not fail on some valid C source files as currently ones do.
Updated by Evgeny Novikov over 5 years ago
- Status changed from New to Resolved
I switched CPAchecker to trunk:30732 in branch frama-c-cil. It seems that the new version takes a bit more resources but sometimes it works better, e.g. there are not some parsing failures and timeouts.
Anyway we will have to switch to the latest version of CPAchecker to get extended witnesses from it.
Updated by Evgeny Novikov over 5 years ago
One our test case failed due to https://gitlab.com/sosy-lab/software/cpachecker/issues/570. It would be better to update CPAchecker one more time rather than to add one more bad preset unknown mark. But I do not know when CPAchecker will be fixed.
Updated by Evgeny Novikov over 5 years ago
Another one bug in CPAchecker is https://gitlab.com/sosy-lab/software/cpachecker/issues/348. One of our validation test case fails due to it. BTW, old CIL replaces enumerators with their values when they are used, so there were not such the bug.
Unfortunately, again we can't rely that somebody will fix this bug in CPAchecker soon.
Updated by Evgeny Novikov over 5 years ago
- Status changed from Resolved to Closed
I merged the branch to master in c082518. Let's wait for CPAchecker fixes separately as it is not known when they will be.