Restrict coverage data to coverage of reachable functions #36
Conversation
| if not reachable_functions: | ||
| return coverage | ||
|
|
||
| def valid_coverage_data(coverage, reachable): |
There was a problem hiding this comment.
What does making this an inline function buy us?
There was a problem hiding this comment.
I don't understand. It is used on only one place. What do you recommend that I do?
There was a problem hiding this comment.
That was just a style question, not a criticism: wrapping it inside a function, vs just inlining the code. I was curious why you'd done the first for code that you only use once.
| return valid | ||
|
|
||
| if not valid_coverage_data(coverage, reachable_functions): | ||
| logging.warning("Coverage calculations may not be accurate") |
There was a problem hiding this comment.
What do we do with these warnings? Does the user see them when they view the report?
There was a problem hiding this comment.
The warnings are printed on the console when we summarize the coverage. Are you advocating that this be encoded in the json so it will appear on the report?
There was a problem hiding this comment.
If possible, yes. Otherwise, a user interacting with the report via CI will not have an easy way to know there were warnings.
There was a problem hiding this comment.
Agree with @danielsn re adding to json.
| @@ -142,12 +143,18 @@ def combine(self, status): | |||
| class Coverage: | |||
| """CBMC coverage checking results""" | |||
|
|
|||
| def __init__(self, coverage_list): | |||
| def __init__(self, coverage_list, viewer_reachable=None): | |||
| """Load CBMC coverage data.""" | |||
|
|
|||
| # TODO: distinguish between coverage of source code and proof code | |||
There was a problem hiding this comment.
Let's create Github issues instead of adding these comments here. #37
| if lines: | ||
| logging.warning( | ||
| "Unreachable function %s has reachable lines %s", | ||
| func_name, ', '.join([str(line) for line in sorted(lines)]) | ||
| ) |
There was a problem hiding this comment.
How can we have a unreachable function with reachable lines?
There was a problem hiding this comment.
I'm concerned about the diffblue tools providing inconsistent information, I tried to drive that home with comments in the code referring to sanity checks.
|
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? |
|
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. |
|
When complete, this pull request should close #69 |
|
Closing as cbmc support has improved since the original submission and there is now an easier implementation |
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