inlined functions are no longer ignored when doing coverage

smowton · Sep 16, 2017 · ac022e2 · ac022e2
1 parent 4cb72b3
commit ac022e2
Show file tree

Hide file tree

Showing 3 changed files with 6 additions and 6 deletions.
diff --git 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
@@ -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
@@ -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())