cbmc-viewer
cbmc-viewer copied to clipboard
Restrict coverage to reachable functions
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.
The listing by goto-instrument has been cleaned up. There is a branch with preliminary work on this, I'll find it.