Feature #11816
closed
Added by Evgeny Novikov about 2 years ago.
Updated about 2 years ago.
Description
Update CPAchecker that started to support packed/aligned attributes (this is a credit of Oleg Petrov and Anton Vasiliev). Several new appropriate test cases are welcome.
- Description updated (diff)
- Status changed from New to Resolved
I updated CPAchecker in branch support-packed-aligned. Besides, I added 2 tests one of which failed before the update of CPAchecker. At last I evaluated changes for drivers of Linux 5.19-rc7 that suffered from the lack of support of packed/aligned attributes. It turned out that most of them become safes/timeouts and there are just 2 unsafes that may be bugs or false alarms due to other reasons. Well done!
I started CI to evaluate the update more comprehensively.
- Status changed from Resolved to Closed
After fixing one issue CI passed tests successfully. Verification of drivers of Linux 5.19-rc7 demonstrated excellent improvements. Unsupported packed/aligned attributes caused ~15% of all false alarms. They all have gone! Moreover, there is no degradations both at checking memory safety and one of the reachability-based requirements specification. I merged the branch to master in f8e6f6e9d.
Also available in: Atom
PDF