replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

inlined functions are no longer ignored when doing coverage

This commit is contained in:
Daniel Kroening 2017-09-09 18:27:04 +01:00
parent 4cb72b3d3e
commit ac022e27ba
3 changed files with 6 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
regression/cbmc-cover/inlining1/main.c
View File

@ -1,3 +1,5 @@
// Discussion point: is the branch below one goal or two?
inline void my_func(int x)
{
if(x)

8
regression/cbmc-cover/inlining1/test.desc
View File

@ -3,9 +3,9 @@ main.c
--cover branch
^EXIT=0$
^SIGNAL=0$
^\[my_func.coverage.1\] file main.c line 3 function my_func block 1 branch false: SATISFIED$
^\[my_func.coverage.2\] file main.c line 3 function my_func block 1 branch true: FAILED$
^\[my_func.coverage.3\] file main.c line 3 function my_func block 2 branch false: FAILED$
^\[my_func.coverage.4\] file main.c line 3 function my_func block 2 branch true: SATISFIED$
^\[main.coverage.1\] file main.c line 13 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$
--
^warning: ignoring

2
src/cbmc/bmc_cover.cpp
View File

@ -204,8 +204,6 @@ bool bmc_covert::operator()()
// This maps property IDs to 'goalt'
forall_goto_functions(f_it, goto_functions)
{
// Functions are already inlined.
if(f_it->second.is_inlined()) continue;
forall_goto_program_instructions(i_it, f_it->second.body)
{
if(i_it->is_assert())