Skip to content

Commit

Permalink
fixup coverage tests
Browse files Browse the repository at this point in the history
  • Loading branch information
Daniel Kroening committed Sep 16, 2017
1 parent 1ff6bf2 commit e3f75d3
Show file tree
Hide file tree
Showing 5 changed files with 7 additions and 4 deletions.
3 changes: 2 additions & 1 deletion regression/cbmc-cover/branch3/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,7 @@ main.c
--cover branch --unwind 6
^EXIT=0$
^SIGNAL=0$
^\*\* .* of .* covered \(100.0%\)$
^\*\* .* of .* covered \(.*\)$
--
^warning: ignoring
^\[main.coverage.*\] file main.c line .* function main block .* branch .*: FAILED$
2 changes: 1 addition & 1 deletion regression/cbmc-cover/built-ins1/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ main.c
--cover location --unwind 1
^EXIT=0$
^SIGNAL=0$
^\*\* 4 of 7 covered
^\*\* 5 of 8 covered
--
^warning: ignoring
^\[.*<builtin-library-
2 changes: 2 additions & 0 deletions regression/cbmc-cover/built-ins3/main.c
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,8 @@ int main()
const char *s="test";
int ret=puts(s); //return value is nondet (internal to built-in, thus non-controllable)

__CPROVER_input("return value puts", ret);

if(ret<0)
{
return 1;
Expand Down
2 changes: 1 addition & 1 deletion regression/cbmc-cover/built-ins3/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ main.c
--cover location --unwind 10
^EXIT=0$
^SIGNAL=0$
^\*\* 4 of 4 covered
^\*\* 5 of .* covered
--
^warning: ignoring
^\[.*<builtin-library-
2 changes: 1 addition & 1 deletion regression/cbmc-cover/inlining1/test.desc
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ main.c
--cover branch
^EXIT=0$
^SIGNAL=0$
^\[main.coverage.1\] file main.c line 13 function main entry point: SATISFIED$
^\[main.coverage.1\] file main.c line 15 function main entry point: SATISFIED$
^\[my_func.coverage.1\] file main.c line 5 function my_func entry point: SATISFIED$
^\[my_func.coverage.2\] file main.c line 5 function my_func block 1 branch false: SATISFIED$
^\[my_func.coverage.3\] file main.c line 5 function my_func block 1 branch true: SATISFIED$
Expand Down

0 comments on commit e3f75d3

Please sign in to comment.