[FEATURE] Coverage measurements from CN

[podhrmic]

Summary

When using CN on a large(r) project (such as OpenSUT), measuring code coverage is important. The following metrics should be useful:

• percentage / LOC of code/functions that have any specs
• any code excluded from CN checking (maybe hiding behind ifdef or some other directive, excluding the code from being examined)
• coverage based on types/classes of specifications (see the different classes we mentioned in the proposal)

Acceptance Criteria

• If CN already provides such metrics, provide documentation how to use it
• if not, develop appropriate metrics as mentioned above
• or provide an external tool (not CN) that can provide such metrics

[podhrmic]

@septract does this sound sensible?

[peterohanley]

We may also want to know which functions have been checked by name. It is possible to use the spec of a function in a header file but not check the function body in another file against that spec, and we'd like to know that this hasn't happened.

[septract]

Yes, this seems like a useful set of measures.

We might also measure the coverage of the specifications themselves. Eg. we can give any function a specification with a false precondition, because this indicates the code cannot be called. But there are more subtle 'bad' specifications which exclude important cases.

This doesn't matter too much for sub-functions, because the specification will be checked at the callsite. So for example, a false precondition will mean a specification cannot be used.

But it becomes very important for top-level specifications where the specification itself is not checked. In this case, a specification may be both true, and allow the function to behave improperly. This is the same as saying the specification does not model the environment properly.

There's a related question whether the post-condition for a top-level specification establishes all the properties that the environment relies on. Eg. the post-condition might only establish True, but perhaps the environment relies on it returning a particular value.

[septract]

A couple of related notions:

1. Various tools try to detect trivial specifications, eg. specifications with false preconditions. E.g I think Dafny does this.
2. We might also check path coverage of specifications. Eg. it might be that some path cannot be exercised under the specification precondition. This might indicate that the spec does not achieve good coverage. But it's subtle - the code might be an error handling path that "should not occur".

[septract]

A technique for performing path coverage for a specification would be to use the property-based testing mechanism (once it exists). Then you would use a standard test coverage measure.

[podhrmic]

@thatplguy this is relevant to the discussion with Jim - what is a good next step towards such measurements? Is this something that CN should do, or some other tool that uses CN should provide?

[septract]

Related: #61