Feature #11782
closed
- Status changed from New to Resolved
I did that in branch update-cif. Let's see on testing results.
- 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).
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.
- Status changed from Open to Resolved
I rebased branch update-cif on top of branch update-cpachecker (#11772, #11833) and launched CI testing.
CI revealed a couple of negative regressions, but they are not crucial. You can see 0d03909c3 for details.
- 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.
Also available in: Atom
PDF