Feature #9532
closed
- 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.
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.
- 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.
Also available in: Atom
PDF