search

model-checking / cbmc-viewer

CBMC Viewer scans the output of CBMC and produces a browsable summary of its findings, making it easy to root cause the issues it finds.
https://model-checking.github.io/cbmc-viewer/
Apache License 2.0
32 stars 11 forks source link

Restrict coverage data to coverage of reachable functions #36

Closed markrtuttle closed 2 years ago

markrtuttle commented 3 years ago

This pull request restricts the coverage calculation and reporting to those functions cbmc considers reachable functions (and not just all functions appearing in the goto binary).

This requires

  1. Adding the set of reachable functions as an optional parameter to the constructors for the various coverage classes (that extract coverage data from the various sources, like xml versus json coverage data).
  2. Moving the computation of reachable functions in the main viewer code to before the computation of the coverage data, and noting the path to the file json file that contains the reachable functions.
  3. Writing a function to filter the coverage data down to the the coverage data for the reachable functions. In the process, we wrote a sanity-checking predicate to confirm that coverage data reports no reachable lines in unreachable functions, and that we have some coverage data for each reachable function.
jimgrundy commented 3 years ago

Can we address the request from @danielsn to get warnings into JSON so they aren't missed by CI users, and the try to advance this PR?

markrtuttle commented 3 years ago

This pull request interacts badly with the --export-file-local flag. The static function foo in file.c is named CPROVER_file_local_file_c_foo in the symbol table with pretty name foo. The --show-reachable-functions flag shows the function reachable with the name __CPROVER_file_local_file_c_foo, but reachable functions skips names with internal prefix CPROVER. On the other hand, coverage data refers to the function as foo and not __CPROVER_file_local_file_c_foo.

Switching to draft pull request until this is fixed.

markrtuttle commented 2 years ago

When complete, this pull request should close https://github.com/model-checking/cbmc-viewer/issues/69

markrtuttle commented 2 years ago

Closing as cbmc support has improved since the original submission and there is now an easier implementation