Skip to content

Commit 639974d

Browse files
author
Daniel Kroening
committed
MC/DC now works
1 parent 3983942 commit 639974d

File tree

3 files changed

+122
-41
lines changed

3 files changed

+122
-41
lines changed

regression/cbmc-cover/mcdc1/main.c

Lines changed: 7 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,16 +1,14 @@
11
int main()
22
{
3-
int input1, input2;
4-
5-
if(input1 && input2)
3+
// Condition and decision coverage can be had with 2 tests,
4+
// but MC/DC needs six (n+1 for n conditions).
5+
6+
__CPROVER_bool A, B, C, D, E;
7+
8+
if ((A || B) && C && D && E)
69
{
7-
// ok
810
}
9-
10-
if(!input1)
11-
input2=1;
12-
13-
if(input1 && input2) // masked!
11+
else
1412
{
1513
}
1614
}

regression/cbmc-cover/mcdc1/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,6 @@ main.c
33
--cover mcdc
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\*\* 17 of 18 covered
6+
^\*\* .* of .* covered (100.0%), using 6 iterations$
77
--
88
^warning: ignoring

src/goto-instrument/cover.cpp

Lines changed: 114 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -64,6 +64,18 @@ class basic_blockst
6464
}
6565
};
6666

67+
/*******************************************************************\
68+
69+
Function: as_string
70+
71+
Inputs:
72+
73+
Outputs:
74+
75+
Purpose:
76+
77+
\*******************************************************************/
78+
6779
const char *as_string(coverage_criteriont c)
6880
{
6981
switch(c)
@@ -82,6 +94,30 @@ const char *as_string(coverage_criteriont c)
8294

8395
/*******************************************************************\
8496
97+
Function: is_condition
98+
99+
Inputs:
100+
101+
Outputs:
102+
103+
Purpose:
104+
105+
\*******************************************************************/
106+
107+
bool is_condition(const exprt &src)
108+
{
109+
if(src.type().id()!=ID_bool) return false;
110+
111+
// conditions are 'atomic predicates'
112+
if(src.id()==ID_and || src.id()==ID_or ||
113+
src.id()==ID_not || src.id()==ID_implies)
114+
return false;
115+
116+
return true;
117+
}
118+
119+
/*******************************************************************\
120+
85121
Function: collect_conditions_rec
86122
87123
Inputs:
@@ -102,22 +138,8 @@ void collect_conditions_rec(const exprt &src, std::set<exprt> &dest)
102138
for(const auto & op : src.operands())
103139
collect_conditions_rec(op, dest);
104140

105-
if(src.type().id()==ID_bool)
106-
{
107-
if(src.id()==ID_and || src.id()==ID_or ||
108-
src.id()==ID_not || src.id()==ID_implies)
109-
{
110-
// ignore me
111-
}
112-
else if(src.is_constant())
113-
{
114-
// ignore me
115-
}
116-
else
117-
{
118-
dest.insert(src);
119-
}
120-
}
141+
if(is_condition(src) && !src.is_constant())
142+
dest.insert(src);
121143
}
122144

123145
/*******************************************************************\
@@ -171,6 +193,29 @@ std::set<exprt> collect_conditions(const goto_programt::const_targett t)
171193

172194
/*******************************************************************\
173195
196+
Function: collect_operands
197+
198+
Inputs:
199+
200+
Outputs:
201+
202+
Purpose:
203+
204+
\*******************************************************************/
205+
206+
void collect_operands(const exprt &src, std::vector<exprt> &dest)
207+
{
208+
for(const exprt &op : src.operands())
209+
{
210+
if(op.id()==src.id())
211+
collect_operands(op, dest);
212+
else
213+
dest.push_back(op);
214+
}
215+
}
216+
217+
/*******************************************************************\
218+
174219
Function: collect_mcdc_controlling_rec
175220
176221
Inputs:
@@ -183,29 +228,67 @@ Function: collect_mcdc_controlling_rec
183228

184229
void collect_mcdc_controlling_rec(
185230
const exprt &src,
231+
const std::vector<exprt> &conditions,
186232
std::set<exprt> &result)
187233
{
188-
if(src.id()==ID_and)
234+
if(src.id()==ID_and ||
235+
src.id()==ID_or)
189236
{
190-
if(src.operands().size()==2)
191-
{
192-
exprt cond1=
193-
conjunction({ src.op0(), not_exprt(src.op1()) });
237+
std::vector<exprt> operands;
238+
collect_operands(src, operands);
194239

195-
exprt cond2=
196-
conjunction({ not_exprt(src.op0()), src.op1() });
240+
if(operands.size()==1)
241+
{
242+
exprt e=*operands.begin();
243+
collect_mcdc_controlling_rec(e, conditions, result);
244+
}
245+
else if(!operands.empty())
246+
{
247+
for(unsigned i=0; i<operands.size(); i++)
248+
{
249+
const exprt op=operands[i];
250+
251+
if(is_condition(op))
252+
{
253+
std::vector<exprt> o=operands;
197254

198-
result.insert(cond1);
199-
result.insert(cond2);
255+
// 'o[i]' needs to be true and false
256+
std::vector<exprt> new_conditions=conditions;
257+
new_conditions.push_back(conjunction(o));
258+
result.insert(conjunction(new_conditions));
259+
260+
o[i].make_not();
261+
new_conditions.back()=conjunction(o);
262+
result.insert(conjunction(new_conditions));
263+
}
264+
else
265+
{
266+
std::vector<exprt> others;
267+
others.reserve(operands.size()-1);
268+
269+
for(unsigned j=0; j<operands.size(); j++)
270+
if(i!=j)
271+
{
272+
if(src.id()==ID_or)
273+
others.push_back(not_exprt(operands[j]));
274+
else
275+
others.push_back(operands[j]);
276+
}
277+
278+
exprt c=conjunction(others);
279+
std::vector<exprt> new_conditions=conditions;
280+
new_conditions.push_back(c);
281+
282+
collect_mcdc_controlling_rec(op, new_conditions, result);
283+
}
284+
}
200285
}
201-
else
202-
collect_mcdc_controlling_rec(make_binary(src), result);
203286
}
204-
else if(src.id()==ID_or)
287+
else if(src.id()==ID_not)
205288
{
289+
exprt e=to_not_expr(src).op();
290+
collect_mcdc_controlling_rec(e, conditions, result);
206291
}
207-
else if(src.id()==ID_not)
208-
collect_mcdc_controlling_rec(to_not_expr(src).op(), result);
209292
}
210293

211294
/*******************************************************************\
@@ -226,7 +309,7 @@ std::set<exprt> collect_mcdc_controlling(
226309
std::set<exprt> result;
227310

228311
for(const auto &d : decisions)
229-
collect_mcdc_controlling_rec(d, result);
312+
collect_mcdc_controlling_rec(d, { }, result);
230313

231314
return result;
232315
}

0 commit comments

Comments
 (0)