Test MC/DC coverage instrumentation

[peterschrammel]

for C programs

[lucasccordeiro]

@kroening: can you please provide some additional information about this task? what is the expected result for testing MC/DC coverage instrumentation? What are the options that we have to use in CBMC? Is there some particular test suite that I should consider?

[kroening]

Please identify suitable publication/reports/definitions with examples to use as tests and identify any existing test suites.

[lucasccordeiro]

@kroening: for a comparator like "x > comparison_point", CBMC is generating 2 test cases to confirm MC/DC: one test case with a TRUE outcome and one test case with a FALSE outcome. Although MC/DC only requires two tests, minimum good requirements-based testing for a comparator would also require 3 additional tests: one input value slightly above, one input value slightly below, and one input value equal to the comparison point. I have talked to Youcheng and it seems that he has already implemented this feature for another project. Should we integrate that code into CBMC?

[kroening]

Yes, but under a different name. What would be the usual name for this?

[lucasccordeiro]

I believe that the usual name in the literature is "boundary testing" or "boundary value analysis". I'll talk to Youcheng so that we can integrate his code into my branch using a different option in CBMC (e.g., "--boundary-testing"). Does it sound OK for you?

[peterschrammel]

It's called boundary value analysis, maybe call it --cover boundary-values?

[kroening]

--cover boundary-values sounds good

[kroening]

There is now the possibility to instrument multiple criteria simultaneously, but there is still interaction between them.

[lucasccordeiro]

Youcheng has mailed me a patch that implements "--cover boundary-values". I'll review it and create another issue in github so that we can track this activity.

[lucasccordeiro]

The option "--cover boundary-values" (implemented by Youcheng) is integrated and tested at:
https://github.com/lucasccordeiro/cbmc/tree/boundary-value-analysis

[kroening]

Can you do a pull request, please?

[lucasccordeiro]

Done.