File tree Expand file tree Collapse file tree 5 files changed +7
-4
lines changed Expand file tree Collapse file tree 5 files changed +7
-4
lines changed Original file line number Diff line number Diff line change 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$
Original file line number Diff line number Diff line change 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-
Original file line number Diff line number Diff 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 ;
Original file line number Diff line number Diff line change 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-
Original file line number Diff line number Diff line change 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$
You can’t perform that action at this time.
0 commit comments