Skip to content

Commit 7b1ca6a

Browse files
kroeningkroening
committed
record the inputs in the tests
1 parent cd81ac9 commit 7b1ca6a

File tree

12 files changed

+50
-26
lines changed

12 files changed

+50
-26
lines changed

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

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,9 @@
11
int main()
22
{
33
int input1, input2;
4+
5+
__CPROVER_input("input1", input1);
6+
__CPROVER_input("input2", input2);
47

58
__CPROVER_assert(!input1, "");
69

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--cover assertion
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main.coverage.1\] file main.c line 5 function main: SATISFIED$
7-
^\[main.coverage.2\] file main.c line 9 function main: SATISFIED$
6+
^\[main.coverage.1\] file main.c line 8 function main: SATISFIED$
7+
^\[main.coverage.2\] file main.c line 12 function main: SATISFIED$
88
--
99
^warning: ignoring

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

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,9 @@ int main()
22
{
33
int input1, input2;
44

5+
__CPROVER_input("input1", input1);
6+
__CPROVER_input("input2", input2);
7+
58
if(input1)
69
{
710
if(input1) // dependent

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

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -4,11 +4,11 @@ main.c
44
^EXIT=0$
55
^SIGNAL=0$
66
^\[main.coverage.1\] file main.c line 3 function main function main entry point: SATISFIED$
7-
^\[main.coverage.2\] file main.c line 5 function main function main block 1 branch false: SATISFIED$
8-
^\[main.coverage.3\] file main.c line 5 function main function main block 1 branch true: SATISFIED$
9-
^\[main.coverage.4\] file main.c line 7 function main function main block 2 branch false: FAILED$
10-
^\[main.coverage.5\] file main.c line 7 function main function main block 2 branch true: SATISFIED$
11-
^\[main.coverage.6\] file main.c line 13 function main function main block 4 branch false: SATISFIED$
12-
^\[main.coverage.7\] file main.c line 13 function main function main block 4 branch true: SATISFIED$
7+
^\[main.coverage.2\] file main.c line 8 function main function main block 1 branch false: SATISFIED$
8+
^\[main.coverage.3\] file main.c line 8 function main function main block 1 branch true: SATISFIED$
9+
^\[main.coverage.4\] file main.c line 10 function main function main block 2 branch false: FAILED$
10+
^\[main.coverage.5\] file main.c line 10 function main function main block 2 branch true: SATISFIED$
11+
^\[main.coverage.6\] file main.c line 16 function main function main block 4 branch false: SATISFIED$
12+
^\[main.coverage.7\] file main.c line 16 function main function main block 4 branch true: SATISFIED$
1313
--
1414
^warning: ignoring

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

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,10 @@
11
int main()
22
{
33
int input1, input2;
4-
4+
5+
__CPROVER_input("input1", input1);
6+
__CPROVER_input("input2", input2);
7+
58
if(input1 && input2)
69
{
710
}

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

Lines changed: 10 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -3,16 +3,16 @@ main.c
33
--cover condition
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main.coverage.1] file main.c line 5 function main condition .* false: SATISFIED
7-
^\[main.coverage.2] file main.c line 5 function main condition .* true: SATISFIED
8-
^\[main.coverage.3] file main.c line 5 function main condition .* false: SATISFIED
9-
^\[main.coverage.4] file main.c line 5 function main condition .* true: SATISFIED
10-
^\[main.coverage.5] file main.c line 8 function main condition .* false: SATISFIED
11-
^\[main.coverage.6] file main.c line 8 function main condition .* true: SATISFIED
12-
^\[main.coverage.7] file main.c line 11 function main condition .* false: SATISFIED
13-
^\[main.coverage.8] file main.c line 11 function main condition .* true: SATISFIED
14-
^\[main.coverage.9] file main.c line 13 function main condition .* false: FAILED
15-
^\[main.coverage.10] file main.c line 13 function main condition .* true: SATISFIED
6+
^\[main.coverage.1] file main.c line 8 function main condition .* false: SATISFIED
7+
^\[main.coverage.2] file main.c line 8 function main condition .* true: SATISFIED
8+
^\[main.coverage.3] file main.c line 8 function main condition .* false: SATISFIED
9+
^\[main.coverage.4] file main.c line 8 function main condition .* true: SATISFIED
10+
^\[main.coverage.5] file main.c line 11 function main condition .* false: SATISFIED
11+
^\[main.coverage.6] file main.c line 11 function main condition .* true: SATISFIED
12+
^\[main.coverage.7] file main.c line 14 function main condition .* false: SATISFIED
13+
^\[main.coverage.8] file main.c line 14 function main condition .* true: SATISFIED
14+
^\[main.coverage.9] file main.c line 16 function main condition .* false: FAILED
15+
^\[main.coverage.10] file main.c line 16 function main condition .* true: SATISFIED
1616
^\*\* 9 of 10 covered (90.0%)
1717
--
1818
^warning: ignoring

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

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,9 @@ int main()
22
{
33
int input1, input2;
44

5+
__CPROVER_input("input1", input1);
6+
__CPROVER_input("input2", input2);
7+
58
__CPROVER_cover(input1);
69
__CPROVER_cover(!input1);
710

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3,9 +3,9 @@ main.c
33
--cover cover
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main.coverage.1] file main.c line 5 function main condition .*: SATISFIED$
7-
^\[main.coverage.2] file main.c line 6 function main condition .*: SATISFIED$
8-
^\[main.coverage.3] file main.c line 10 function main condition .*: FAILED$
6+
^\[main.coverage.1] file main.c line 8 function main condition .*: SATISFIED$
7+
^\[main.coverage.2] file main.c line 9 function main condition .*: SATISFIED$
8+
^\[main.coverage.3] file main.c line 13 function main condition .*: FAILED$
99
^\*\* 2 of 3 covered (66.7%), using .* iterations$
1010
--
1111
^warning: ignoring

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

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,10 @@ int main()
22
{
33
int input1, input2, input3;
44

5+
__CPROVER_input("input1", input1);
6+
__CPROVER_input("input2", input2);
7+
__CPROVER_input("input3", input3);
8+
59
if(input1 && input2 && input3)
610
{
711
}

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

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,8 @@ int main()
33
int input1;
44
int x=0;
55

6+
__CPROVER_input("input1", input1);
7+
68
if(input1)
79
{
810
x=1;

0 commit comments

Comments
 (0)