Remove the __CPROVER_HIDE label when inlining

Leaving this label in place will mark the function being inlined into as hidden,
which messes up, e.g., coverage instrumentation.

Consider hidden.c:

 #include <string.h>
 int foo() { char *a, *b; return memcmp(a, b, 1); }
 int main() { foo(); return 0; }

goto-cc hidden.c
goto-instrument --add-library a.out b.out (add library function with hiding)
goto-analyzer --simplify c.out b.out (goto-analyzer does inlining)
cbmc --cover location c.out (will be missing any coverage targets in foo)
cbmc --cover location b.out (has coverage targets in foo)

With this patch, cbmc --cover location c.out also has coverage targets in foo.

Author: tautschnig

src/goto-programs/goto_inline_class.cpp

@@ -285,6 +285,13 @@ void goto_inlinet::insert_function_body(
     for(auto &instruction : body.instructions)
       instruction.function=target->function;
 
+  // make sure the inlined function does not introduce hiding
+  if(goto_function.is_hidden())
+  {
+    for(auto &instruction : body.instructions)
+      instruction.labels.remove("__CPROVER_HIDE");
+  }
+
   replace_return(body, lhs);
 
   goto_programt tmp1;