Project

General

Profile

Feature #9532

Bug #6629: Used CIL is outdated

Update CPAchecker

Added by Evgeny Novikov 9 months ago. Updated 9 months ago.

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

0%

Estimated time:
Published in build:

Description

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

History

#1

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

#2

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

#3

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

#4

Updated by Evgeny Novikov 9 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