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.
Category:
Environment models
Description
Corresponding false alarms constitute ~5% of all false alarms at verification of Linux kernel drivers, so this issue deserves an appropriate attention.
- 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.
- 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.
Also available in: Atom
PDF