why need unwind only to run coverage
Closed this issue · 4 comments
CBMC version: 5.82
Operating system:
Exact command line resulting in the issue: cbmc -gcc xx.c --cover mcdc
What behaviour did you expect: i think only run coverage dont need unwind
What happened instead:
cbmc will unwind xx.c first, then ouput coverage info.
Perhaps our expectations on what "coverage" means differ? CBMC will prove reachability of locations/branches/mcdc conditions, i.e., will demonstrate that there exists an execution where these can be reached. To arrive at these proofs, CBMC uses symbolic execution, which requires iterating over loops (among other things).
Would you mind elaborating what notion of coverage you expected?
@tautschnig Just like gcov can get coverage by running the compiled program directly, I think coverage should be achieved by running the code under test.
Perhaps there is a misunderstanding of what CBMC does? CBMC will only ever symbolically "run" your program, and unwinding (i.e., iterating through loops) is doing exactly that.
I think this has basically been answered. We can't analyse for coverage correctly without unwinding as the algorithm we use for the coverage analysis depends on it. A concrete execution performed by gcov will cover a single execution path / set of values for each point in time. A cbmc coverage analysis using symbolic execution is reasoning about what could be reached for any execution path or any set of input values. As such this is a different kind of analysis, with different requirements and subtly different meaning to the output generated.
The value to a gcov analysis would be to tell you what your existing automated tests cover. The value in a cbmc coverage analysis is that it gives an indication of what execution paths/locations cbmc can analyse in conjunction with the assertions in the code under analysis.
Given this hasn't been commented on further for the past week, I am going to close out this issue. Feel free to re-open if you need to discus this further.