Klever incorrectly shows coverage in libraries at visualization of error traces
Motivation example: drivers/uwb/hwa-rc.ko (linux:memory safety)
There is a library function "interface_to_usbdev" in source files/include/linux/usb.h at 613-616 lines.
Actual coverage from CPAchecker says that both lines and the function are covered but coverage JSON does not contain the coverage for this file at all. Thus, a user see misleading results.
Updated by Ilja Zakharov 15 days ago
- Assignee set to Vladimir Gratinskiy
- Category changed from Results processing to Bridge
Seems that reason of this issue is a bug in Bridge. Bridge at error trace visualization should not highlight with the red color any files which are not referred in coverage report. But it does it both for header files and outside C files which are not included into the verification task.
Updated by Evgeny Novikov 15 days ago
Yes, we agreed that Bridge should show empty code coverage just for those source files that are presented in coverage statistics and for which there are zeroes. Other source files, that are reachable through cross references, should not be shown as non-covered. Otherwise, users do not understand code coverage semantics easily.