Feature #9532

Bug #6629: Used CIL is outdated

Update CPAchecker

Added by Evgeny Novikov 11 months ago. Updated 10 months ago.

Target version:
Start date:
Due date:
% Done:


Estimated time:
Published in build:


New versions of CPAchecker will not fail on some valid C source files as currently ones do.



Updated by Evgeny Novikov 11 months 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 10 months ago

One our test case failed due to 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 10 months ago

Another one bug in CPAchecker is 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 10 months 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.

Also available in: Atom PDF