From f2306e3372041b75d79e06fa4cb844d69e04f8db Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 8 Oct 2018 18:53:54 +0000 Subject: [PATCH] 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 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. --- src/goto-programs/goto_inline_class.cpp | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/goto-programs/goto_inline_class.cpp b/src/goto-programs/goto_inline_class.cpp index fdf4721e036..8219befbe8b 100644 --- a/src/goto-programs/goto_inline_class.cpp +++ b/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;