diff --git a/regression/cbmc-cover/inlining1/main.c b/regression/cbmc-cover/inlining1/main.c index c15b715bc7..ac37bc65f2 100644 --- a/regression/cbmc-cover/inlining1/main.c +++ b/regression/cbmc-cover/inlining1/main.c @@ -1,3 +1,5 @@ +// Discussion point: is the branch below one goal or two? + inline void my_func(int x) { if(x) diff --git a/regression/cbmc-cover/inlining1/test.desc b/regression/cbmc-cover/inlining1/test.desc index 1c2f5cff9f..f9f0e95caa 100644 --- a/regression/cbmc-cover/inlining1/test.desc +++ b/regression/cbmc-cover/inlining1/test.desc @@ -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 diff --git a/src/cbmc/bmc_cover.cpp b/src/cbmc/bmc_cover.cpp index c0ad5465c6..bc772e5960 100644 --- a/src/cbmc/bmc_cover.cpp +++ b/src/cbmc/bmc_cover.cpp @@ -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())