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 to reachable functions #69

Open markrtuttle opened 2 years ago

markrtuttle commented 2 years ago

We should restrict coverage to the reachable functions. Currently coverage checking reports coverage on all code, not just the statically reachable code. Prior attempts to restrict to reachable functions were broken by the used of --export-file-local-symbols because goto-analysis was reporting the mangled name and coverage data was reporting the unmangled name.

This is important because proof writers use --remove-function-body excessively to clean up the coverage reports. This would make that unnecessary.

markrtuttle commented 2 years ago

The listing by goto-instrument has been cleaned up. There is a branch with preliminary work on this, I'll find it.