[klee-dev] Option for generating MC/DC test cases

[Damir]

>
> I disagree with your conclusion.
>
> The test cases which you have declared inconsistent with MC/DC are
> consistent with my understanding of MC/DC (as applied to C).
>
You are right, what  you describe is called Short-circuit MC/DC.
I found a very interesting paper about Short-circuit MC/DC and MCC
(Multiple Condition Coverage), here:
http://link.springer.com/article/10.1007/s00607-014-0418-5

Basically, for non-short-circuit languages like Ada, MCC with N conditions
requires 2^n testcases. But, as shown in abovementioned paper, for
short-circuit languages, MCC is only a little worse in terms of number of
testcases than MC/DC (which is minumum n+1 testcases), so it can be
practical to aim to MCC instead. MCC is a superset of MC/DC.

So, returning to klee and CIL, I can provide you with another
counterexample, taken directly from aforementioned paper.

Condition is now  (a && b || c) (or with extra paretheses for readability,
(a && b) || c).

Basic klee testcases:
(0 0 0)
(0 0 1) (just decision coverage)

Cilly + klee testcases:
(1 1 0)
 (0 0 0)
 (0 0 1) - (condition coverage and decision coverage)

As you can see, CIL + klee cannot provide enough  testcases in this case,
it should include (1, 0, 0) for short-circuit MC/DC.

Basically, this is what CIL does to the condition:
it replaces

if (a && b || c)
      do_then();
else
      do_else();

with following:

if (a) {
   if (b) {
         do_then();
   }
   else
         goto check_C;
}
else
check_C:
if (c) {
    do_then();
}
else
   do_else();

But, if I manually replace "goto check_C" with a copy of the code after
that label, klee is finally able to produce 5 testcases:
(0 0 0)
(0 0 1)
(1 1 0)
(1 0 1)
(1 0 0)

As you can see, those 5 testcases produce short-circuit MCC, which is a
superset of short-circuit MC/DC! That's why you told me earlier that
testcases by cilly + klee will be a superset of MC/DC.

Unfortunatley, that's not the case, cilly + klee alone cannot produce the
desired testcases, but that just gave me an idea of how klee can be changed
to produce short-circuit MCC instead of just decision coverage. It just
needs not to filter out the testcases that were covering the same block,
but came through different paths during evaluation of short-circuit boolean
expression.

I will run some tests and will get back with the results.
-------------- next part --------------
HTML attachment scrubbed and removed