Project

General

Profile

Actions

Bug #9847

closed

Klever incorrectly shows coverage in libraries at visualization of error traces

Added by Ilja Zakharov about 5 years ago. Updated almost 5 years ago.

Status:
Closed
Priority:
Urgent
Category:
Bridge
Target version:
Start date:
10/04/2019
Due date:
% Done:

0%

Estimated time:
Detected in build:
svn
Platform:
Published in build:

Description

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.


Files

coverage.info (63 KB) coverage.info Ilja Zakharov, 10/04/2019 03:59 PM
coverage-verification.zip (1.57 KB) coverage-verification.zip Ilja Zakharov, 10/04/2019 03:59 PM

Related issues 1 (0 open1 closed)

Precedes Klever - Feature #9866: Show warning when users will reach source files without code coverageClosedVladimir Gratinskiy10/07/201912/03/2019

Actions
Actions #1

Updated by Ilja Zakharov about 5 years ago

  • Category changed from Results processing to Bridge
  • Assignee set to Vladimir Gratinskiy

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.

Actions #2

Updated by Evgeny Novikov about 5 years 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.

Actions #3

Updated by Evgeny Novikov about 5 years ago

Moreover, I suggest to show an explicit warning when users will reach source files without code coverage. This warning may be the following: "You can try another code coverage type to get code coverage for a given source file".

Actions #4

Updated by Vladimir Gratinskiy about 5 years ago

  • Priority changed from Urgent to Normal

Implemented in klever-3.0, but without an explicit warning.

Actions #5

Updated by Evgeny Novikov about 5 years ago

  • Status changed from New to Resolved
  • Priority changed from Normal to Urgent

Okay, let's think about warnings one day later. There are many other places where some help for users is strictly necessary as well.

Actions #6

Updated by Evgeny Novikov about 5 years ago

  • Precedes Feature #9866: Show warning when users will reach source files without code coverage added
Actions #7

Updated by Evgeny Novikov almost 5 years ago

  • Status changed from Resolved to Closed

In master.

Actions

Also available in: Atom PDF