Skip to content

Commit e3f75d3

Browse files
author
Daniel Kroening
committed
fixup coverage tests
1 parent 1ff6bf2 commit e3f75d3

File tree

5 files changed

+7
-4
lines changed

5 files changed

+7
-4
lines changed

regression/cbmc-cover/branch3/test.desc

+2-1
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@ main.c
33
--cover branch --unwind 6
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\*\* .* of .* covered \(100.0%\)$
6+
^\*\* .* of .* covered \(.*\)$
77
--
88
^warning: ignoring
9+
^\[main.coverage.*\] file main.c line .* function main block .* branch .*: FAILED$

regression/cbmc-cover/built-ins1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--cover location --unwind 1
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\*\* 4 of 7 covered
6+
^\*\* 5 of 8 covered
77
--
88
^warning: ignoring
99
^\[.*<builtin-library-

regression/cbmc-cover/built-ins3/main.c

+2
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,8 @@ int main()
55
const char *s="test";
66
int ret=puts(s); //return value is nondet (internal to built-in, thus non-controllable)
77

8+
__CPROVER_input("return value puts", ret);
9+
810
if(ret<0)
911
{
1012
return 1;

regression/cbmc-cover/built-ins3/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--cover location --unwind 10
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\*\* 4 of 4 covered
6+
^\*\* 5 of .* covered
77
--
88
^warning: ignoring
99
^\[.*<builtin-library-

regression/cbmc-cover/inlining1/test.desc

+1-1
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ main.c
33
--cover branch
44
^EXIT=0$
55
^SIGNAL=0$
6-
^\[main.coverage.1\] file main.c line 13 function main entry point: SATISFIED$
6+
^\[main.coverage.1\] file main.c line 15 function main entry point: SATISFIED$
77
^\[my_func.coverage.1\] file main.c line 5 function my_func entry point: SATISFIED$
88
^\[my_func.coverage.2\] file main.c line 5 function my_func block 1 branch false: SATISFIED$
99
^\[my_func.coverage.3\] file main.c line 5 function my_func block 1 branch true: SATISFIED$

0 commit comments

Comments
 (0)