replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

use apply in cover_util 

This avoids the case split over the instruction type.
This commit is contained in:
Daniel Kroening 2019-05-01 12:16:03 +01:00
parent 12f1571a55
commit 3e8b9d9240
5 changed files with 26 additions and 83 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
regression/cbmc-cover/mcdc1/test.desc
View File

@ -3,12 +3,12 @@ main.c
--cover mcdc
^EXIT=0$
^SIGNAL=0$
^\[main.coverage.1\] file main.c line 14 function main MC/DC independence condition `C && D && !E && A && !B.*: SATISFIED$
^\[main.coverage.2\] file main.c line 14 function main MC/DC independence condition `C && !D && E && A && !B.*: SATISFIED$
^\[main.coverage.3\] file main.c line 14 function main MC/DC independence condition `!C && D && E && A && !B.*: SATISFIED$
^\[main.coverage.4\] file main.c line 14 function main MC/DC independence condition `C && D && E && A && !B.*: SATISFIED$
^\[main.coverage.5\] file main.c line 14 function main MC/DC independence condition `C && D && E && !A && B.*: SATISFIED$
^\[main.coverage.6\] file main.c line 14 function main MC/DC independence condition `C && D && E && !A && !B.*: SATISFIED$
^\[main.coverage.\d+\] file main.c line 14 function main MC/DC independence condition `C && D && !E && A && !B.*: SATISFIED$
^\[main.coverage.\d+\] file main.c line 14 function main MC/DC independence condition `C && !D && E && A && !B.*: SATISFIED$
^\[main.coverage.\d+\] file main.c line 14 function main MC/DC independence condition `!C && D && E && A && !B.*: SATISFIED$
^\[main.coverage.\d+\] file main.c line 14 function main MC/DC independence condition `C && D && E && A && !B.*: SATISFIED$
^\[main.coverage.\d+\] file main.c line 14 function main MC/DC independence condition `C && D && E && !A && B.*: SATISFIED$
^\[main.coverage.\d+\] file main.c line 14 function main MC/DC independence condition `C && D && E && !A && !B.*: SATISFIED$
^\*\* .* of .* covered \(100.0%\)$
--
^warning: ignoring

8
regression/cbmc-cover/mcdc2/test.desc
View File

@ -3,10 +3,10 @@ main.c
--cover mcdc
^EXIT=0$
^SIGNAL=0$
^\[main.coverage.1\] file main.c line 10 function main MC/DC independence condition `A && !B && !C.*: SATISFIED$
^\[main.coverage.2\] file main.c line 10 function main MC/DC independence condition `!A && B && !C.*: SATISFIED$
^\[main.coverage.3\] file main.c line 10 function main MC/DC independence condition `!A && !B && C.*: SATISFIED$
^\[main.coverage.4\] file main.c line 10 function main MC/DC independence condition `!A && !B && !C.*: SATISFIED$
^\[main.coverage.\d+\] file main.c line 10 function main MC/DC independence condition `A && !B && !C.*: SATISFIED$
^\[main.coverage.\d+\] file main.c line 10 function main MC/DC independence condition `!A && B && !C.*: SATISFIED$
^\[main.coverage.\d+\] file main.c line 10 function main MC/DC independence condition `!A && !B && C.*: SATISFIED$
^\[main.coverage.\d+\] file main.c line 10 function main MC/DC independence condition `!A && !B && !C.*: SATISFIED$
^\*\* .* of .* covered \(100.0%\)$
--
^warning: ignoring

10
regression/cbmc-cover/mcdc4/test.desc
View File

@ -3,11 +3,11 @@ main.c
--cover mcdc
^EXIT=0$
^SIGNAL=0$
^\[main.coverage.1\] file main.c line 11 function main MC/DC independence condition `A && B && C && !D.*: SATISFIED$
^\[main.coverage.2\] file main.c line 11 function main MC/DC independence condition `A && !B && C && D.*: SATISFIED$
^\[main.coverage.3\] file main.c line 11 function main MC/DC independence condition `A && !B && C && !D.*: SATISFIED$
^\[main.coverage.4\] file main.c line 11 function main MC/DC independence condition `!C && D && A && !B.*: SATISFIED$
^\[main.coverage.5\] file main.c line 11 function main MC/DC independence condition `!A && B && C && !D.*: SATISFIED$
^\[main.coverage.\d+\] file main.c line 11 function main MC/DC independence condition `A && B && C && !D.*: SATISFIED$
^\[main.coverage.\d+\] file main.c line 11 function main MC/DC independence condition `A && !B && C && D.*: SATISFIED$
^\[main.coverage.\d+\] file main.c line 11 function main MC/DC independence condition `A && !B && C && !D.*: SATISFIED$
^\[main.coverage.\d+\] file main.c line 11 function main MC/DC independence condition `!C && D && A && !B.*: SATISFIED$
^\[main.coverage.\d+\] file main.c line 11 function main MC/DC independence condition `!A && B && C && !D.*: SATISFIED$
^\*\* .* of .* covered \(100.0%\)$
--
^warning: ignoring

10
regression/cbmc-cover/mcdc5/test.desc
View File

@ -3,11 +3,11 @@ main.c
--cover mcdc
^EXIT=0$
^SIGNAL=0$
^\[main.coverage.1\] file main.c line 10 function main MC/DC independence condition `A && !B && C && !D.*: SATISFIED$
^\[main.coverage.2\] file main.c line 10 function main MC/DC independence condition `!C && D && A && !B.*: SATISFIED$
^\[main.coverage.3\] file main.c line 10 function main MC/DC independence condition `!C && !D && A && !B.*: SATISFIED$
^\[main.coverage.4\] file main.c line 10 function main MC/DC independence condition `!A && B && C && !D.*: SATISFIED$
^\[main.coverage.5\] file main.c line 10 function main MC/DC independence condition `!A && !B && C && !D.*: SATISFIED$
^\[main.coverage.\d+\] file main.c line 10 function main MC/DC independence condition `A && !B && C && !D.*: SATISFIED$
^\[main.coverage.\d+\] file main.c line 10 function main MC/DC independence condition `!C && D && A && !B.*: SATISFIED$
^\[main.coverage.\d+\] file main.c line 10 function main MC/DC independence condition `!C && !D && A && !B.*: SATISFIED$
^\[main.coverage.\d+\] file main.c line 10 function main MC/DC independence condition `!A && B && C && !D.*: SATISFIED$
^\[main.coverage.\d+\] file main.c line 10 function main MC/DC independence condition `!A && !B && C && !D.*: SATISFIED$
^\*\* .* of .* covered \(100.0%\)$
--
^warning: ignoring

69
src/goto-instrument/cover_util.cpp
View File

@ -48,36 +48,11 @@ std::set<exprt> collect_conditions(const exprt &src)
std::set<exprt> collect_conditions(const goto_programt::const_targett t)
{
switch(t->type)
{
case GOTO:
case ASSERT:
return collect_conditions(t->guard);
std::set<exprt> result;
case ASSIGN:
case FUNCTION_CALL:
return collect_conditions(t->code);
t->apply([&result](const exprt &e) { collect_conditions_rec(e, result); });
case CATCH:
case THROW:
case DEAD:
case DECL:
case RETURN:
case ATOMIC_BEGIN:
case ATOMIC_END:
case START_THREAD:
case END_THREAD:
case END_FUNCTION:
case LOCATION:
case OTHER:
case SKIP:
case ASSUME:
case INCOMPLETE_GOTO:
case NO_INSTRUCTION_TYPE:
break;
}
return std::set<exprt>();
return result;
}
void collect_operands(const exprt &src, std::vector<exprt> &dest)
@ -120,43 +95,11 @@ void collect_decisions_rec(const exprt &src, std::set<exprt> &dest)
}
}
std::set<exprt> collect_decisions(const exprt &src)
{
std::set<exprt> result;
collect_decisions_rec(src, result);
return result;
}
std::set<exprt> collect_decisions(const goto_programt::const_targett t)
{
switch(t->type)
{
case GOTO:
case ASSERT:
return collect_decisions(t->guard);
std::set<exprt> result;
case ASSIGN:
case FUNCTION_CALL:
return collect_decisions(t->code);
t->apply([&result](const exprt &e) { collect_decisions_rec(e, result); });
case CATCH:
case THROW:
case DEAD:
case DECL:
case RETURN:
case ATOMIC_BEGIN:
case ATOMIC_END:
case START_THREAD:
case END_THREAD:
case END_FUNCTION:
case LOCATION:
case OTHER:
case SKIP:
case ASSUME:
case INCOMPLETE_GOTO:
case NO_INSTRUCTION_TYPE:
break;
}
return std::set<exprt>();
return result;
}