Skip to content

Commit 3983942

Browse files
author
Daniel Kroening
committed
more MC/DC
1 parent 49c1acf commit 3983942

File tree

3 files changed

+41
-1
lines changed

3 files changed

+41
-1
lines changed

regression/cbmc-cover/mcdc1/main.c

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,16 @@
1+
int main()
2+
{
3+
int input1, input2;
4+
5+
if(input1 && input2)
6+
{
7+
// ok
8+
}
9+
10+
if(!input1)
11+
input2=1;
12+
13+
if(input1 && input2) // masked!
14+
{
15+
}
16+
}

regression/cbmc-cover/mcdc1/test.desc

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
CORE
2+
main.c
3+
--cover mcdc
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\*\* 17 of 18 covered
7+
--
8+
^warning: ignoring

src/goto-instrument/cover.cpp

Lines changed: 17 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ Date: May 2016
1111
#include <algorithm>
1212

1313
#include <util/i2string.h>
14+
#include <util/expr_util.h>
1415

1516
#include "cover.h"
1617

@@ -186,6 +187,19 @@ void collect_mcdc_controlling_rec(
186187
{
187188
if(src.id()==ID_and)
188189
{
190+
if(src.operands().size()==2)
191+
{
192+
exprt cond1=
193+
conjunction({ src.op0(), not_exprt(src.op1()) });
194+
195+
exprt cond2=
196+
conjunction({ not_exprt(src.op0()), src.op1() });
197+
198+
result.insert(cond1);
199+
result.insert(cond2);
200+
}
201+
else
202+
collect_mcdc_controlling_rec(make_binary(src), result);
189203
}
190204
else if(src.id()==ID_or)
191205
{
@@ -532,8 +546,10 @@ void instrument_cover_goals(
532546

533547
for(const auto & p : controlling)
534548
{
549+
std::string p_string=from_expr(ns, "", p);
550+
535551
std::string description=
536-
"MC/DC independence condition";
552+
"MC/DC independence condition `"+p_string+"'";
537553

538554
goto_program.insert_before_swap(i_it);
539555
i_it->make_assertion(p);

0 commit comments

Comments
 (0)