CBMC's Condition Coverage (--cover condition) produces inverted results. #8722
Description
There is a bug in CBMC's condition coverage functionality that leads to erroneous results.
For example, in the simple program below.
int main() {
int x = 5;
if (x == 5) {
return 1;
}
return 0;
}Since x is always equal to 5, if we execute cbmc --cover condition to get the true and false satisfiability of the program's condition, we would expect that the true branch of the condition x == 5 should be satisfied, and the false branch should never be satisfied.
However, running cbmc --cover condition <filename.c> produces:
CBMC version 6.3.1 (cbmc-6.3.1) 64-bit x86_64 linux
[Removed intermediate lines]
SAT checker: instance is SATISFIABLE
** coverage results:
[main.coverage.1] file cbmc6_harness.c line 5 function main condition 'x == 5' false: SATISFIED
[main.coverage.2] file cbmc6_harness.c line 5 function main condition 'x == 5' true: FAILED
** 1 of 2 covered (50.0%)
On the contrary, the MC/DC coverage tool produces the inverse (and correct) result.
Running cbmc --cover mcdc <filename.c> yields:
SAT checker: instance is SATISFIABLE
** coverage results:
[main.coverage.1] file cbmc6_harness.c line 5 function main decision/condition 'x == 5' false: FAILED
[main.coverage.2] file cbmc6_harness.c line 5 function main decision/condition 'x == 5' true: SATISFIED
** 1 of 2 covered (50.0%)
After debugging (and with GitHub Copilot's help navigating the complex codebase), I realized this error is caused by differences in how the coverage assertion instrumentation in the condition and MC/DC coverage tools are implemented.
Specifically, for the MC/DC coverage, to determine if a condition (true path) is satisfiable, we invert the condition and hence, any counter-example means there is a path through the program that satisfies the condition.
std::string comment_t = description + " '" + p_string + "' true";
...
*i_it = make_assertion(not_exprt(p), annotated_location);On the contrary, the condition coverage implementation does not invert the asserted condition, leading to the inverted result.
const std::string comment_t = "condition '" + c_string + "' true";
...
*i_it = make_assertion(c, source_location);