MC/DC (Modified Condition/Decision Coverage)¶

Statement coverage¶

The statement coverage measures the proportion of statements reached during analyses.

For one analysis, the detailed statement coverage is provided in the -info-statements results, a summary by function is available in the -info-functions results, and an overall summary is available in the -info-results results.

For several analyses, tis-aggregate coverage can be used (see tis-aggregate Manual) and tis-report HTML result can be browsed to explore the results.

A 100% statement coverage is quite easy to reach. For instance, on the following example:

int D;
void f (int a, int b) {
  if (a && b)
    D = 1;
  else
    D = 0;
}

A 100% statement coverage is reached with these two calls, despite a is always 1:

int main (void) {
Tf1: f(1, 1);
Tf2: f(1, 0);
}

This can be check with the commands:

$ tis-analyzer --interpreter -info-json-results main1_results.json -info-csv-all main1 main1.c
$ jq .coverage < main1_results.json
{
  "type": "informative",
  "function_coverage": "100%",
  "total_statements_coverage": "100%",
  "semantic_statements_coverage": "100%"
}

Branch coverage¶

The branch coverage, often named CC for Condition Coverage, checks that each (elementary) condition can be evaluated at least one time true and one time false during tests.

Information about branch coverage can be found in the More column of the -info-statements results.

On the previous example:

$ tis-analyzer --interpreter -info-json-results main1_results.json -info-csv-all main1 main1.c
$ grep ', test,' main1_statements.csv | cut -d, -f4,5,6,10,11
 f, 1, reachable, test, else branch dead
 f, 2, reachable, test, 

As expected, this result shows that the else branch of the first test (i.e. a) has not been analyzed.

To reach the 100% branch coverage, the test Tf3 has to be added:

int main (void) {
Tf1: f(1, 1);
Tf2: f(1, 0);
Tf3: f(0, 0);
}

Now, with the same commands as before, we can check that both branches of both tests are analyzed (the More column is empty):

$ tis-analyzer --interpreter -info-json-results main2_results.json -info-csv-all main2 main2.c
$ grep ', test,' main2_statements.csv | cut -d, -f4,5,6,10,11
 f, 1, reachable, test, 
 f, 2, reachable, test, 

The DC (Decision Coverage) tells that each decision (combination of conditions) has to be evaluated at least one time true and one time false during tests. The theory says that CC can be satisfied without DC being satisfied. The given example (from Wikipedia) is that for the decision (a and b), the tests (a=true, b=false) and (a=false, b=true) satisfy CC, but not DC since the decision is not true for either tests. But in a C program, the b=true branch is not covered because, since a=false in the second test, the b condition is not evaluated. So, for C programs, CC implies DC.

The term Condition/decision coverage (C/DC) is also used to tell that both decision and condition coverage are satisfied.

MC/DC coverage¶

The Modified condition/decision coverage is stronger. It requires C/DC and also that in every decision, each boolean condition has been changed independently to the others, and that it changes the decision. In other words, it means that, if a decision, composed of n boolean conditions, is reached with the condition values (b1, ..., bn), then is has to be also reached with values (b1', ..., bn') where only one bi' different from bi (all the others being equal), and moreover, the decision (i.e. branch taken) must be different.

Let’s consider the following example:

int D;
void g (int a, int b, int c) {
  if ((a || b) && c)
    D = 1;
  else
    D = 0;
}

And let’s analyze with the following tests:

int main (void) {
Tg1: g (1, 1, 1); //@ assert D == 1;
Tg2: g (0, 0, 0); //@ assert D == 0;
Tg3: g (0, 1, 0); //@ assert D == 0;
}

We can check that C/DC is reached:

$ tis-analyzer --interpreter -info-json-results main3_results.json -info-csv-all main3 main3.c
$ jq .coverage < main3_results.json
{
  "type": "informative",
  "function_coverage": "100%",
  "total_statements_coverage": "100%",
  "semantic_statements_coverage": "100%"
}
$ grep ', test,' main3_statements.csv | cut -d, -f4,5,6,10,11
 g, 1, reachable, test, 
 g, 3, reachable, test, 
 g, 5, reachable, test, 

But about MC/DC, at a first glance, we can observe that:

• a is not changed alone,
• b is changed alone between T2 and T3, but the decision is the same for these two tests (D == 0),
• c is not changed alone.

Notice that, because of how the decisions are computed in C, not all the conditions are always evaluated. So, for instance, in T1, since if a is true, the value of b is not meaningful. It is similar in T2: because both a and b are false, then the first part of the conjunction is false, the value of c is also meaningless.

So, the example is equivalent to the one above it the tests are changed into:

extern int x;

int main (void) {
Tg1: g (1, x, 1); //@ assert D == 1;
Tg2: g (0, 0, x); //@ assert D == 0;
Tg3: g (0, 1, 0); //@ assert D == 0;
}

In that case, the MC/DC evaluation is a little better than before because:

• about a modification, b must be 0 and c must be 1 to make the value of a matter, so, considering the x value, the decision is modified in T1 and T2 where only a changes;
• about b and c, some tests are still missing.

Let’s examine all the possible tests for this example:

So, to reach the MC/DC criteria, we can for instance consider the following tests:

• about a modification: as seen before, T1 and T2 can be considered
• about b modification: a must be 0 and c must be 1 to make the value of b matter, so, T4 has to be added and paired with T2
• about c modification: T3 and T4 fulfill the requirements.

So, adding T4 is enough to reach the MC/DC criteria.

Reducing the computation¶

The ideas presented below are inspired by the article *Formalization and Comparison of MCDC and Object Branch Coverage Criteria* (from AdaCore in 2012).

This paper proves that:

• in some cases, branch coverage implies MC/DC,
• in other cases, we know for sure that the branch coverage may be reached without having MC/DC.

This is a representation of the (a && b) decision:

A similar graph may be drawn to represent a (a || b) decision.

In both cases, each condition has (at least) a branch that gives the value of the decision (let’s call it the direct output of the condition). Considering the cases where a decision is only composed of such conditions, we can prove that if we have a test set that ensure branch coverage, then MC/DC is reached.

This is because, considering any condition C of the decision:

• there is only one set of evaluation of the previous conditions that lead to C,
• since both branches of C are covered, there are at least two tests that reach C, but with different values for C
• if the direct output of C lead to a decision D, there is for sure an instantiation of the conditions after C that lead to the opposite decision.

This situation happens if the decision is only built with only one kind of operator, either && or ||. So these decisions are very easy to identify, and there is nothing more to compute in those cases. Moreover, the paper states that the other tests are not very frequent (they say 1% on industrial applications).

But anyway, let’s examine the second case when the operators are mixed.

For instance, the example ((a || b) && c) already seen above can be represented by:

In this case, where at least one of the condition has at least two predecessors (c in this example), we can prove that there exists a set of tests that covers all the branches, but for which MD/MC is not reached.

Let’s consider a condition C that has two predecessors, and the last condition C’ either leads to C, or have a direct output (this is b in the example above). Let’s build the following test set:

• add the tests that cover the C’ direct output, where the decision is D.
• add tests that cover C’ other branch (leading to C) but only with branches leading to D
• add tests that cover the other branch leading to C (branch from a to c in the example) and that lead to the other decision (!D).

Now, we have a set of tests that covers all the branches, but MC/DC is not satisfied because all the test where only C’ is modified lead to the same decision D.

So, the conclusion is:

• examining the branch coverage of decisions involving only one kind of boolean operator is enough for MC/DC
• but it is not enough to rely on the branch coverage to evaluate MC/DC on decisions that mix different boolean operators: in that case, studying the traces for each computation of the decision is required.

To know how the kind of information that are collected and exported, refer to the About the Decisions section in the Tis-info Manual, and to find out how they are used to evaluate MC/DC from several analyses results, see Modified condition/decision coverage in the Tis-aggregate Manual.