Project

General

Profile

Actions
Copy link

Feature #9532

closed

Bug #6629: Used CIL is outdated

Update CPAchecker

Added by Evgeny Novikov over 5 years ago. Updated over 5 years ago.

Status:
Closed
Priority:
Urgent
Assignee:
Evgeny Novikov
Category:
Addons
Target version:
3.0
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.

Actions
Copy link
 #1

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.

Actions
Copy link
 #2

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.

Actions
Copy link
 #3

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.

Actions
Copy link
 #4

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.

Actions
Copy link

Also available in: Atom PDF