Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Improved MCDC coverage #195

Merged
merged 9 commits into from
Aug 18, 2016
Merged

Improved MCDC coverage #195

Show file tree
Hide file tree
Changes from 4 commits
Commits
Show all changes
9 commits
Select commit Hold shift + click to select a range
c29c44e
Improved the implementation of "--cover mcdc".
theyoucheng Aug 9, 2016
b4c8ec5
Added test cases for mcdc coverage.
theyoucheng Aug 9, 2016
32a1078
Updated the test.desc file of test case cbmc-cover/mcdc1/
theyoucheng Aug 9, 2016
c7343b3
Refactored the code for mcdc coverage; added a debug test case "cbmc-…
theyoucheng Aug 9, 2016
e520282
Added more comments; formatted several functions; removed dangling if…
theyoucheng Aug 10, 2016
a0d01d0
formatted
theyoucheng Aug 10, 2016
18c4d53
Do not directly handle an atomic condition within "collect_mcdc_contr…
theyoucheng Aug 11, 2016
8af80a7
When evaluating the value of an expr, the result now will be among +1…
theyoucheng Aug 11, 2016
9090532
Removed dangling if-else statements.
theyoucheng Aug 11, 2016
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions regression/cbmc-cover/mcdc1/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,4 +17,6 @@ int main()
else
{
}

return 1;
}
8 changes: 7 additions & 1 deletion regression/cbmc-cover/mcdc1/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,13 @@ 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$
^\*\* .* of .* covered (100.0%)$
^\*\* Used 6 iterations$
^\*\* Used 10 iterations$
--
^warning: ignoring
18 changes: 18 additions & 0 deletions regression/cbmc-cover/mcdc2/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
int main()
{

__CPROVER_bool A, B, C;

__CPROVER_input("A", A);
__CPROVER_input("B", B);
__CPROVER_input("C", C);

if(A||B||C)
{
}
else
{
}

return 1;
}
13 changes: 13 additions & 0 deletions regression/cbmc-cover/mcdc2/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
CORE
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$
^\*\* .* of .* covered (100.0%)$
^\*\* Used 6 iterations$
--
^warning: ignoring
8 changes: 8 additions & 0 deletions regression/cbmc-cover/mcdc3/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
int main()
{
unsigned x, y;
if (!(x>3) && y<5)
;

return 1;
}
12 changes: 12 additions & 0 deletions regression/cbmc-cover/mcdc3/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
CORE
main.c
--cover mcdc
^EXIT=0$
^SIGNAL=0$
^\[main.coverage.1\] file main.c line 4 function main MC/DC independence condition `!(x > (unsigned int)3) && !(y < (unsigned int)5).*: SATISFIED$
^\[main.coverage.2\] file main.c line 4 function main MC/DC independence condition `y < (unsigned int)5 && !(x > (unsigned int)3).*: SATISFIED$
^\[main.coverage.3\] file main.c line 4 function main MC/DC independence condition `y < (unsigned int)5 && x > (unsigned int)3.*: SATISFIED$
^\*\* .* of .* covered (100.0%)$
^\*\* Used 4 iterations$
--
^warning: ignoring
19 changes: 19 additions & 0 deletions regression/cbmc-cover/mcdc4/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
int main()
{

__CPROVER_bool A, B, C, D;

__CPROVER_input("A", A);
__CPROVER_input("B", B);
__CPROVER_input("C", C);
__CPROVER_input("D", D);

if((A && B) || (C && D))
{
}
else
{
}

return 1;
}
14 changes: 14 additions & 0 deletions regression/cbmc-cover/mcdc4/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
CORE
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$
^\*\* .* of .* covered (100.0%)$
^\*\* Used 9 iterations$
--
^warning: ignoring
18 changes: 18 additions & 0 deletions regression/cbmc-cover/mcdc5/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
int main()
{
__CPROVER_bool A, B, C, D;

__CPROVER_input("A", A);
__CPROVER_input("B", B);
__CPROVER_input("C", C);
__CPROVER_input("D", D);

if((A || B) && (C || D))
{
}
else
{
}

return 1;
}
14 changes: 14 additions & 0 deletions regression/cbmc-cover/mcdc5/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
CORE
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$
^\*\* .* of .* covered (100.0%)$
^\*\* Used 9 iterations$
--
^warning: ignoring
8 changes: 8 additions & 0 deletions regression/cbmc-cover/mcdc6/main.c
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
int main()
{
unsigned x;
if(x<3)
;

return 1;
}
11 changes: 11 additions & 0 deletions regression/cbmc-cover/mcdc6/test.desc
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
CORE
main.c
--cover mcdc
^EXIT=0$
^SIGNAL=0$
^\[main.coverage.1\] file main.c line 4 function main MC/DC independence condition `!(x < (unsigned int)3).*: SATISFIED$
^\[main.coverage.2\] file main.c line 4 function main MC/DC independence condition `x < (unsigned int)3.*: SATISFIED$
^\*\* .* of .* covered (100.0%)$
^\*\* Used 2 iterations$
--
^warning: ignoring
Loading