Project

General

Profile

Actions
Copy link

Feature #11793

closed

Add models and tests for v4l2_device_(un)register()

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

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

0%

Estimated time:
Published in build:

Description

Corresponding false alarms constitute ~5% of all false alarms at verification of Linux kernel drivers, so this issue deserves an appropriate attention.

Actions
Copy link
 #1

Updated by Evgeny Novikov over 2 years ago

  • Status changed from New to Resolved

I add models and tests for v4l2_device_(un)register() in branch v4l2_device_models_and_tests. Preliminary evaluation on corresponding false alarms demonstrated that they all become either safes or timeouts. Let's run all tests.

Actions
Copy link
 #2

Updated by Evgeny Novikov over 2 years ago

  • Status changed from Resolved to Closed

Extended testing demonstrated even more positive regressions. Both configurations of CPAchecker, that are used in Klever, improved verification results. 2 assertions became timeouts while 1 timeout became unsafe (target bug). Besides, verification of ~1600 drivers of Linux 5.19 demonstrated several transitions from unknowns (timeouts) to unsafes that are primarily false alarms due to some issues in CPAchecker SMG.

I merged the branch to master in 3ecf59177.

Actions
Copy link

Also available in: Atom PDF