"--cover and --unwinding-assertions must not be given together"

[tedinski]

CBMC version: latest / any / 5.43
Operating system: any
Exact command line resulting in the issue: cbmc --unwinding-assertions --cover location ...
What behaviour did you expect: CBMC would run and give me coverage information
What happened instead: Failed to run with the error "--cover and --unwinding-assertions must not be given together"

Use case: RMC has a default set of flags that we pass to CBMC that includes --unwinding-assertions to enforce soundness. To use cbmc-viewer we need three runs of cbmc using (1) --trace (2) --cover location (3) --show-properties.

I acknowledge that the "correct" fix here is to break up our default set of flags into groups that are appropriate for each invocation of cbmc. (We're clearly enabling too much redundant work right now by turning on a bunch of default assertions for the coverage invocation.) But I initially just tried cbmc <default-args> <additional flag> and was perplexed by this error.

I don't understand why this combination of flags is disallowed. If I look back through commit history, I see the original introduction here:

b200bbd

But this initially just silently disables unwinding-assertions when cover is enabled, (perhaps because they're harmlessly redundant?) This turned into an error here:

#2049

But I'm not sure this combination should be disallowed at all. Is there any harm in instrumenting both of these assertions at the same time? (I haven't investigated, but this might be the only meaningful obstacle to getting failure and coverage in one run of cbmc instead of needing two, and that might be an even more "correct" fix...)

[martin-cs]

I don't know if this is helpful but some context. --unwinding-assertions is a very old option, well, originally it was --no-unwinding-assertions as the default was to have them so that you knew when the results were incomplete. The default got flipped because it was so common that people would use it and complete unwinding was rare (in cases where it was not expected). It wasn't quite an assertion in the classic sense but it was ... similar enough that it could be treated as one. IIRC at this point CBMC was just returning one failing assertion by default. Hence why --no-unwinding-assertions.

The cover options are more recent and were extensively reworked by Diffblue (IIRC @peterschrammel did the design). As these where "good" assertions and you wanted to cover as many of them as you could, so using the cover options did a bunch of other things, like requesting all solutions, ignoring other assertions (maybe even --assert-to-assume) and disabling unwinding-assertions. I know around this time there was some dispute over the semantics of assertion and what happens after them, which has very big consequences for how you do coverage instrumentation ( see #2031 and 92b92d6 ).

I don't see any reason in principle why one could not handle program assertions, instrumented assertions, coverage assertions and unwinding assertions all together in a uniform way. But maybe some of the Diffblue folks ( @peterschrammel @chrisr-diffblue ? ) could chime in as they are big users of the --cover options.

[peterschrammel]

I don't see any apparent reason why --unwinding-assertions couldn't be handled when running with --cover. However, one needs to be careful when integrating it into a loop that automatically increments --unwind as the reporting is different with --cover due to the reversed semantics of assertions. As @martin-cs explained, hitting a coverage goal means failing an assertion, which is something good.