cbmc-viewer icon indicating copy to clipboard operation
cbmc-viewer copied to clipboard

Restrict coverage to reachable functions

Open markrtuttle opened this issue 3 years ago • 1 comments

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 avatar Dec 07 '21 15:12 markrtuttle

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

markrtuttle avatar Dec 07 '21 15:12 markrtuttle