fix for inlining

Author: Daniel Kroening

regression/cbmc-cover/inlining1/main.c

@@ -0,0 +1,15 @@
+inline void my_func(int x)
+{
+  if(x)
+  {
+  }
+  else
+  {
+  }
+}
+
+int main()
+{
+  my_func(0);
+  my_func(1);
+}

regression/cbmc-cover/inlining1/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--cover branch
+^EXIT=0$
+^SIGNAL=0$
+^\[my_func.coverage.1\] file main.c line 3 function my_func function my_func block 1 branch false: SATISFIED$
+^\[my_func.coverage.2\] file main.c line 3 function my_func function my_func block 1 branch true: FAILED$
+^\[my_func.coverage.3\] file main.c line 3 function my_func function my_func block 2 branch false: FAILED$
+^\[my_func.coverage.4\] file main.c line 3 function my_func function my_func block 2 branch true: SATISFIED$
+--
+^warning: ignoring

regression/cbmc-cover/location11/test.desc

@@ -3,17 +3,17 @@ main.c
 --cover location
 ^EXIT=0$
 ^SIGNAL=0$
-\[main.coverage.1\] file main.c line 11 function main block 1: SATISFIED
-\[main.coverage.2\] file main.c line 13 function main block 2: FAILED
-\[main.coverage.3\] file main.c line 13 function main block 3: FAILED
-\[main.coverage.4\] file main.c line 15 function main block 4: SATISFIED
-\[main.coverage.5\] file main.c line 17 function main block 5: SATISFIED
-\[main.coverage.6\] file main.c line 18 function main block 6: SATISFIED
-\[main.coverage.7\] file main.c line 20 function main block 7: FAILED
-\[main.coverage.8\] file main.c line 22 function main block 8: SATISFIED
-\[main.coverage.9\] file main.c line 23 function main block 9: SATISFIED
-\[myfunc.coverage.1\] file main.c line 5 function myfunc block 1: FAILED
-\[myfunc.coverage.2\] file main.c line 7 function myfunc block 2: FAILED
+^\[main.coverage.1\] file main.c line 11 function main block 1: SATISFIED$
+^\[main.coverage.2\] file main.c line 13 function main block 2: FAILED$
+^\[main.coverage.3\] file main.c line 13 function main block 3: FAILED$
+^\[main.coverage.4\] file main.c line 15 function main block 4: SATISFIED$
+^\[main.coverage.5\] file main.c line 17 function main block 5: SATISFIED$
+^\[main.coverage.6\] file main.c line 18 function main block 6: SATISFIED$
+^\[main.coverage.7\] file main.c line 20 function main block 7: FAILED$
+^\[main.coverage.8\] file main.c line 22 function main block 8: SATISFIED$
+^\[main.coverage.9\] file main.c line 23 function main block 9: SATISFIED$
+^\[myfunc.coverage.1\] file main.c line 5 function myfunc block 1: FAILED$
+^\[myfunc.coverage.2\] file main.c line 7 function myfunc block 2: FAILED$
 ^\*\* 6 of 11 covered \(54.5%\)
 --
 ^warning: ignoring

regression/cbmc-cover/location14/test.desc

@@ -3,13 +3,13 @@ main.c
 --cover location
 ^EXIT=0$
 ^SIGNAL=0$
-\[main.coverage.1\] file main.c line 10 function main block 1: SATISFIED
-\[main.coverage.2\] file main.c line 12 function main block 2: FAILED
-\[main.coverage.3\] file main.c line 12 function main block 3: FAILED
-\[main.coverage.4\] file main.c line 12 function main block 4: FAILED
-\[main.coverage.5\] file main.c line 13 function main block 6: SATISFIED
-\[foo.coverage.1\] file main.c line 5 function foo block 1: FAILED
-\[foo.coverage.2\] file main.c line 6 function foo block 2: FAILED
+^\[main.coverage.1\] file main.c line 10 function main block 1: SATISFIED$
+^\[main.coverage.2\] file main.c line 12 function main block 2: FAILED$
+^\[main.coverage.3\] file main.c line 12 function main block 3: FAILED$
+^\[main.coverage.4\] file main.c line 12 function main block 4: FAILED$
+^\[main.coverage.5\] file main.c line 13 function main block 6: SATISFIED$
+^\[foo.coverage.1\] file main.c line 5 function foo block 1: FAILED$
+^\[foo.coverage.2\] file main.c line 6 function foo block 2: FAILED$
 ^\*\* 2 of 7 covered \(28.6%\)
 --
 ^warning: ignoring

src/cbmc/bmc_cover.cpp

@@ -235,6 +235,8 @@ 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())