Skip to content

Commit 3b4214e

Browse files
lucasccordeirolucasccordeiro
committed
add test cases to check MC/DC coverage instrumentation
Signed-off-by: Lucas Cordeiro <[email protected]>
1 parent f496571 commit 3b4214e

File tree

14 files changed

+252
-0
lines changed

14 files changed

+252
-0
lines changed

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

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
int main()
2+
{
3+
_Bool A, B, C;
4+
5+
__CPROVER_input("cold", A);
6+
__CPROVER_input("raining", B);
7+
__CPROVER_input("windy", C);
8+
9+
if ( A || B || C )
10+
{
11+
/* instructions */
12+
}
13+
else
14+
{
15+
/* instructions */
16+
}
17+
18+
return 1;
19+
}

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

Lines changed: 13 additions & 0 deletions
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 9 function main MC/DC independence condition `A != FALSE && !(B != FALSE) && !(C != FALSE).*: SATISFIED$
7+
^\[main.coverage.2\] file main.c line 9 function main MC/DC independence condition `!(A != FALSE) && B != FALSE && !(C != FALSE).*: SATISFIED$
8+
^\[main.coverage.3\] file main.c line 9 function main MC/DC independence condition `!(A != FALSE) && !(B != FALSE) && C != FALSE.*: SATISFIED$
9+
^\[main.coverage.4\] file main.c line 9 function main MC/DC independence condition `!(A != FALSE) && !(B != FALSE) && !(C != FALSE).*: SATISFIED$
10+
^\*\* .* of .* covered (100.0%)$
11+
^\*\* Used 5 iterations$
12+
--
13+
^warning: ignoring

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

Lines changed: 27 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,27 @@
1+
int main()
2+
{
3+
_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)
11+
{
12+
if (C || D)
13+
{
14+
/* instructions */
15+
}
16+
else
17+
{
18+
/* instructions */
19+
}
20+
}
21+
else
22+
{
23+
/* instructions */
24+
}
25+
26+
return 1;
27+
}

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

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
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 != FALSE && B != FALSE.*: SATISFIED$
7+
^\[main.coverage.2\] file main.c line 10 function main MC/DC independence condition `A != FALSE && !(B != FALSE).*: SATISFIED$
8+
^\[main.coverage.3\] file main.c line 10 function main MC/DC independence condition `!(A != FALSE) && B != FALSE.*: SATISFIED$
9+
^\[main.coverage.10\] file main.c line 12 function main MC/DC independence condition `C != FALSE && !(D != FALSE).*: SATISFIED$
10+
^\[main.coverage.11\] file main.c line 12 function main MC/DC independence condition `!(C != FALSE) && D != FALSE.*: SATISFIED$
11+
^\[main.coverage.12\] file main.c line 12 function main MC/DC independence condition `!(C != FALSE) && !(D != FALSE).*: SATISFIED$
12+
^\*\* .* of .* covered (100.0%)$
13+
^\*\* Used 6 iterations$
14+
--
15+
^warning: ignoring

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

Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,36 @@
1+
int main()
2+
{
3+
_Bool A, B, C, D, E, F;
4+
5+
__CPROVER_input("A", A);
6+
__CPROVER_input("B", B);
7+
__CPROVER_input("C", C);
8+
__CPROVER_input("D", D);
9+
__CPROVER_input("E", D);
10+
__CPROVER_input("F", D);
11+
12+
if (A && B)
13+
{
14+
if (C || D)
15+
{
16+
/* instructions */
17+
}
18+
else
19+
{
20+
/* instructions */
21+
}
22+
}
23+
else
24+
{
25+
if (E || F)
26+
{
27+
/* instructions */
28+
}
29+
else
30+
{
31+
/* instructions */
32+
}
33+
}
34+
35+
return 1;
36+
}

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

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

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

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
int main()
2+
{
3+
_Bool A, B, C;
4+
5+
__CPROVER_input("A", A);
6+
__CPROVER_input("B", B);
7+
__CPROVER_input("C", C);
8+
9+
if (A && B && C)
10+
{
11+
/* instructions */
12+
}
13+
14+
return 1;
15+
}

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

Lines changed: 13 additions & 0 deletions
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 9 function main MC/DC independence condition `A != FALSE && B != FALSE && C != FALSE.* SATISFIED$
7+
^\[main.coverage.2\] file main.c line 9 function main MC/DC independence condition `A != FALSE && B != FALSE && !(C != FALSE).* SATISFIED$
8+
^\[main.coverage.3\] file main.c line 9 function main MC/DC independence condition `A != FALSE && !(B != FALSE) && C != FALSE.* SATISFIED$
9+
^\[main.coverage.4\] file main.c line 9 function main MC/DC independence condition `!(A != FALSE) && B != FALSE && C != FALSE.* SATISFIED$
10+
^\*\* .* of .* covered (100.0%)$
11+
^\*\* Used 6 iterations$
12+
--
13+
^warning: ignoring

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

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
int main()
2+
{
3+
int altitude;
4+
5+
__CPROVER_input("altitude", altitude);
6+
7+
if (altitude > 2500)
8+
{
9+
/* instructions */
10+
}
11+
12+
return 1;
13+
}

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

Lines changed: 11 additions & 0 deletions
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 7 function main decision/condition `altitude > 2500.* SATISFIED$
7+
^\[main.coverage.2\] file main.c line 7 function main decision/condition `altitude > 2500.* SATISFIED$
8+
^\*\* .* of .* covered (100.0%)$
9+
^\*\* Used 2 iterations$
10+
--
11+
^warning: ignoring

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

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
int main()
2+
{
3+
_Bool a, b, c;
4+
5+
__CPROVER_input("a", a);
6+
__CPROVER_input("b", b);
7+
__CPROVER_input("c", c);
8+
9+
if ( (a || b) && c )
10+
{
11+
/* instructions */
12+
}
13+
else
14+
{
15+
/* instructions */
16+
}
17+
18+
return 1;
19+
}

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

Lines changed: 13 additions & 0 deletions
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 9 function main MC/DC independence condition `c != FALSE && a != FALSE && !(b != FALSE).* SATISFIED$
7+
^\[main.coverage.2\] file main.c line 9 function main MC/DC independence condition `c != FALSE && !(a != FALSE) && b != FALSE.* SATISFIED$
8+
^\[main.coverage.3\] file main.c line 9 function main MC/DC independence condition `c != FALSE && !(a != FALSE) && !(b != FALSE).* SATISFIED$
9+
^\[main.coverage.4\] file main.c line 9 function main MC/DC independence condition `!(c != FALSE) && a != FALSE && !(b != FALSE).* SATISFIED$
10+
^\*\* .* of .* covered (100.0%)$
11+
^\*\* Used 6 iterations$
12+
--
13+
^warning: ignoring

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

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
int main()
2+
{
3+
_Bool u, x, y, z;
4+
_Bool A, B, C, D;
5+
6+
A = (u==0);
7+
B = (x>5);
8+
C = (y<6);
9+
D = (z==0);
10+
11+
__CPROVER_input("A", A);
12+
__CPROVER_input("B", B);
13+
__CPROVER_input("C", C);
14+
__CPROVER_input("D", D);
15+
16+
if ( (A || B) && (C || D) )
17+
{
18+
/* instructions */
19+
}
20+
else
21+
{
22+
/* instructions */
23+
}
24+
25+
return 1;
26+
}

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

Lines changed: 14 additions & 0 deletions
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.9\] file main.c line 16 function main MC/DC independence condition `A != FALSE && !(B != FALSE) && C != FALSE && !(D != FALSE).* SATISFIED$
7+
^\[main.coverage.10\] file main.c line 16 function main MC/DC independence condition `!(C != FALSE) && D != FALSE && A != FALSE && !(B != FALSE).* SATISFIED$
8+
^\[main.coverage.11\] file main.c line 16 function main MC/DC independence condition `!(C != FALSE) && !(D != FALSE) && A != FALSE && !(B != FALSE).* SATISFIED$
9+
^\[main.coverage.12\] file main.c line 16 function main MC/DC independence condition `!(A != FALSE) && B != FALSE && C != FALSE && !(D != FALSE).* SATISFIED$
10+
^\[main.coverage.13\] file main.c line 16 function main MC/DC independence condition `!(A != FALSE) && !(B != FALSE) && C != FALSE && !(D != FALSE).* SATISFIED$
11+
^\*\* .* of .* covered (100.0%)$
12+
^\*\* Used 8 iterations$
13+
--
14+
^warning: ignoring

0 commit comments

Comments
 (0)