Project

General

Profile

Actions
Copy link

Feature #11816

closed

Update CPAchecker

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

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

0%

Estimated time:
Published in build:

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.

Actions
Copy link
 #1

Updated by Evgeny Novikov over 2 years ago

  • Description updated (diff)
Actions
Copy link
 #2

Updated by Evgeny Novikov over 2 years ago

  • 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.

Actions
Copy link
 #3

Updated by Evgeny Novikov over 2 years ago

  • 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.

Actions
Copy link

Also available in: Atom PDF