Feature #11782
closedUpdate CIF
0%
Description
There are some fixes and improvements in CIF, so let's update it in Klever.
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.
Updated by Evgeny Novikov over 2 years ago
- Blocked by Feature #11772: Update CPAchecker added
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).
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.
Updated by Evgeny Novikov over 2 years ago
- Blocked by Feature #11833: Update CPAchecker added
Updated by Evgeny Novikov over 2 years ago
- Status changed from Open to Resolved
Updated by Evgeny Novikov over 2 years ago
CI revealed a couple of negative regressions, but they are not crucial. You can see 0d03909c3 for details.
Updated by Evgeny Novikov over 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.