Skip to content

Commit 8bc9b29

Browse files
author
Daniel Kroening
authored
Merge pull request #195 from theyoucheng/mcdc
Improved MCDC coverage
2 parents 42cc9b9 + 9090532 commit 8bc9b29

File tree

15 files changed

+814
-7
lines changed

15 files changed

+814
-7
lines changed

‎regression/cbmc-cover/mcdc1/main.c

+2
Original file line numberDiff line numberDiff line change
@@ -17,4 +17,6 @@ int main()
1717
else
1818
{
1919
}
20+
21+
return 1;
2022
}

‎regression/cbmc-cover/mcdc1/test.desc

+7-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,13 @@ main.c
33
--cover mcdc
44
^EXIT=0$
55
^SIGNAL=0$
6+
^\[main.coverage.1\] file main.c line 14 function main MC/DC independence condition `C && D && !E && A && !B.*: SATISFIED$
7+
^\[main.coverage.2\] file main.c line 14 function main MC/DC independence condition `C && !D && E && A && !B.*: SATISFIED$
8+
^\[main.coverage.3\] file main.c line 14 function main MC/DC independence condition `!C && D && E && A && !B.*: SATISFIED$
9+
^\[main.coverage.4\] file main.c line 14 function main MC/DC independence condition `C && D && E && A && !B.*: SATISFIED$
10+
^\[main.coverage.5\] file main.c line 14 function main MC/DC independence condition `C && D && E && !A && B.*: SATISFIED$
11+
^\[main.coverage.6\] file main.c line 14 function main MC/DC independence condition `C && D && E && !A && !B.*: SATISFIED$
612
^\*\* .* of .* covered (100.0%)$
7-
^\*\* Used 6 iterations$
13+
^\*\* Used 10 iterations$
814
--
915
^warning: ignoring

‎regression/cbmc-cover/mcdc2/main.c

+18
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
int main()
2+
{
3+
4+
__CPROVER_bool A, B, C;
5+
6+
__CPROVER_input("A", A);
7+
__CPROVER_input("B", B);
8+
__CPROVER_input("C", C);
9+
10+
if(A||B||C)
11+
{
12+
}
13+
else
14+
{
15+
}
16+
17+
return 1;
18+
}

‎regression/cbmc-cover/mcdc2/test.desc

+13
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
main.c
3+
--cover mcdc
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main.coverage.1\] file main.c line 10 function main MC/DC independence condition `A && !B && !C.*: SATISFIED$
7+
^\[main.coverage.2\] file main.c line 10 function main MC/DC independence condition `!A && B && !C.*: SATISFIED$
8+
^\[main.coverage.3\] file main.c line 10 function main MC/DC independence condition `!A && !B && C.*: SATISFIED$
9+
^\[main.coverage.4\] file main.c line 10 function main MC/DC independence condition `!A && !B && !C.*: SATISFIED$
10+
^\*\* .* of .* covered (100.0%)$
11+
^\*\* Used 6 iterations$
12+
--
13+
^warning: ignoring

‎regression/cbmc-cover/mcdc3/main.c

+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
int main()
2+
{
3+
unsigned x, y;
4+
if (!(x>3) && y<5)
5+
;
6+
7+
return 1;
8+
}

‎regression/cbmc-cover/mcdc3/test.desc

+12
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
main.c
3+
--cover mcdc
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main.coverage.1\] file main.c line 4 function main MC/DC independence condition `!(x > (unsigned int)3) && !(y < (unsigned int)5).*: SATISFIED$
7+
^\[main.coverage.2\] file main.c line 4 function main MC/DC independence condition `y < (unsigned int)5 && !(x > (unsigned int)3).*: SATISFIED$
8+
^\[main.coverage.3\] file main.c line 4 function main MC/DC independence condition `y < (unsigned int)5 && x > (unsigned int)3.*: SATISFIED$
9+
^\*\* .* of .* covered (100.0%)$
10+
^\*\* Used 4 iterations$
11+
--
12+
^warning: ignoring

‎regression/cbmc-cover/mcdc4/main.c

+19
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
int main()
2+
{
3+
4+
__CPROVER_bool A, B, C, D;
5+
6+
__CPROVER_input("A", A);
7+
__CPROVER_input("B", B);
8+
__CPROVER_input("C", C);
9+
__CPROVER_input("D", D);
10+
11+
if((A && B) || (C && D))
12+
{
13+
}
14+
else
15+
{
16+
}
17+
18+
return 1;
19+
}

‎regression/cbmc-cover/mcdc4/test.desc

+14
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
CORE
2+
main.c
3+
--cover mcdc
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main.coverage.1\] file main.c line 11 function main MC/DC independence condition `A && B && C && !D.*: SATISFIED$
7+
^\[main.coverage.2\] file main.c line 11 function main MC/DC independence condition `A && !B && C && D.*: SATISFIED$
8+
^\[main.coverage.3\] file main.c line 11 function main MC/DC independence condition `A && !B && C && !D.*: SATISFIED$
9+
^\[main.coverage.4\] file main.c line 11 function main MC/DC independence condition `!C && D && A && !B.*: SATISFIED$
10+
^\[main.coverage.5\] file main.c line 11 function main MC/DC independence condition `!A && B && C && !D.*: SATISFIED$
11+
^\*\* .* of .* covered (100.0%)$
12+
^\*\* Used 9 iterations$
13+
--
14+
^warning: ignoring

‎regression/cbmc-cover/mcdc5/main.c

+18
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
int main()
2+
{
3+
__CPROVER_bool A, B, C, D;
4+
5+
__CPROVER_input("A", A);
6+
__CPROVER_input("B", B);
7+
__CPROVER_input("C", C);
8+
__CPROVER_input("D", D);
9+
10+
if((A || B) && (C || D))
11+
{
12+
}
13+
else
14+
{
15+
}
16+
17+
return 1;
18+
}

‎regression/cbmc-cover/mcdc5/test.desc

+14
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
CORE
2+
main.c
3+
--cover mcdc
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main.coverage.1\] file main.c line 10 function main MC/DC independence condition `A && !B && C && !D.*: SATISFIED$
7+
^\[main.coverage.2\] file main.c line 10 function main MC/DC independence condition `!C && D && A && !B.*: SATISFIED$
8+
^\[main.coverage.3\] file main.c line 10 function main MC/DC independence condition `!C && !D && A && !B.*: SATISFIED$
9+
^\[main.coverage.4\] file main.c line 10 function main MC/DC independence condition `!A && B && C && !D.*: SATISFIED$
10+
^\[main.coverage.5\] file main.c line 10 function main MC/DC independence condition `!A && !B && C && !D.*: SATISFIED$
11+
^\*\* .* of .* covered (100.0%)$
12+
^\*\* Used 9 iterations$
13+
--
14+
^warning: ignoring

‎regression/cbmc-cover/mcdc6/main.c

+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
int main()
2+
{
3+
unsigned x;
4+
if(x<3)
5+
;
6+
7+
return 1;
8+
}

‎regression/cbmc-cover/mcdc6/test.desc

+11
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
main.c
3+
--cover mcdc
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main.coverage.1\] file main.c line 4 function main decision/condition `x < (unsigned int)3.* false: SATISFIED$
7+
^\[main.coverage.2\] file main.c line 4 function main decision/condition `x < (unsigned int)3.* true: SATISFIED$
8+
^\*\* .* of .* covered (100.0%)$
9+
^\*\* Used 2 iterations$
10+
--
11+
^warning: ignoring

‎regression/cbmc-cover/mcdc7/main.c

+8
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,8 @@
1+
int main()
2+
{
3+
signed x, y;
4+
5+
y = x*123<0 ? 0 : (x*123>100 ? 100 : x*123 );
6+
7+
return 1;
8+
}

‎regression/cbmc-cover/mcdc7/test.desc

+13
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
main.c
3+
--cover mcdc
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
^\[main.coverage.1\] file main.c line 5 function main decision/condition `x \* 123 > 100.* false: SATISFIED$
7+
^\[main.coverage.2\] file main.c line 5 function main decision/condition `x \* 123 > 100.* true: SATISFIED$
8+
^\[main.coverage.3\] file main.c line 5 function main decision/condition `x \* 123 < 0.* false: SATISFIED$
9+
^\[main.coverage.4\] file main.c line 5 function main decision/condition `x \* 123 < 0.* true: SATISFIED$
10+
^\*\* .* of .* covered (100.0%)$
11+
^\*\* Used 2 iterations$
12+
--
13+
^warning: ignoring

0 commit comments

Comments
 (0)