Project

General

Profile

Actions
Copy link

Feature #11782

closed

Update CIF

Added by Evgeny Novikov over 2 years ago. Updated about 2 years ago.

Status:
Closed
Priority:
High
Assignee:
Evgeny Novikov
Category:
Addons
Target version:
3.7
Start date:
07/26/2022
Due date:
% Done:

0%

Estimated time:
Published in build:

Description

There are some fixes and improvements in CIF, so let's update it in Klever.

Related issues 2 (0 open — 2 closed)

Blocked by Klever - Feature #11772: Update CPAcheckerClosedEvgeny Novikov07/21/2022

Actions
Blocked by Klever - Feature #11833: Update CPAcheckerClosedEvgeny Novikov08/17/2022

Actions
Actions
Copy link
 #1

Updated by Evgeny Novikov over 2 years ago

  • Status changed from New to Resolved

I did that in branch update-cif. Let's see on testing results.

Actions
Copy link
 #2

Updated by Evgeny Novikov over 2 years ago

Actions
Copy link
 #3

Updated by Evgeny Novikov over 2 years ago

  • Status changed from Resolved to Open

It turned out that CPAchecker could not spit out error traces containing local static variables (it runs out of heap memory after a long period of time). Thus, it is necessary to fix and update it first (#11772).

Actions
Copy link
 #4

Updated by Evgeny Novikov over 2 years ago

Ilya has recently fixed warning from Clang-Tidy (https://github.com/ldv-klever/cif/pull/3). This should not affect anything anyhow, so I included the corresponding update into the branch for upcoming testing.

Actions
Copy link
 #5

Updated by Evgeny Novikov about 2 years ago

Actions
Copy link
 #6

Updated by Evgeny Novikov about 2 years ago

  • Status changed from Open to Resolved

I rebased branch update-cif on top of branch update-cpachecker (#11772, #11833) and launched CI testing.

Actions
Copy link
 #7

Updated by Evgeny Novikov about 2 years ago

CI revealed a couple of negative regressions, but they are not crucial. You can see 0d03909c3 for details.

Actions
Copy link
 #8

Updated by Evgeny Novikov about 2 years ago

  • Status changed from Resolved to Closed

Verification of a subset of Linux 5.19-rc7 drivers showed a bunch of improvements. The overall CPU time consumed by CPAchecker decreased for ~10%! Correspondingly a lot of timeouts became pretty hard safes and unsafes (some of these unsafes were already revealed early). Thus, a minor fix can result in great improvements. I merged the branch to master in commit:c0d03909c3.

Actions
Copy link

Also available in: Atom PDF