Merge pull request #6338 from tautschnig/fix-6330-part-2

goto-analyzer --(un)reachable-functions should not rely on base names

Author: tautschnig

regression/goto-cc-goto-analyzer/reachable-functions-export-file-local-symbols/project.c

@@ -0,0 +1,9 @@
+static int foo(int x)
+{
+  return x + 1;
+}
+
+static int bar(int x)
+{
+  return x + 2;
+}

regression/goto-cc-goto-analyzer/reachable-functions-export-file-local-symbols/proof.c

@@ -0,0 +1,7 @@
+int __CPROVER_file_local_project_c_foo(int x);
+
+int main()
+{
+  int x = __CPROVER_file_local_project_c_foo(1);
+  assert(x == 2);
+}

regression/goto-cc-goto-analyzer/reachable-functions-export-file-local-symbols/test.desc

@@ -0,0 +1,13 @@
+CORE
+test.c
+--reachable-functions
+^.* foo 1 4$
+^EXIT=0$
+^SIGNAL=0$
+--
+^.* [a-zA-Z0-9_]+foo \d+ \d+$
+--
+This test checks that after building the goto binary (see test.sh) with
+--export-file-local-symbols function "foo" is still reported as reachable. Note,
+that the symbol representing "foo" has a mangled name in the goto binary, which
+makes the symbol name different from its base name.

regression/goto-cc-goto-analyzer/reachable-functions-export-file-local-symbols/test.sh

@@ -0,0 +1,15 @@
+#!/usr/bin/env bash
+set -e
+
+goto_cc=$1
+is_windows=$2
+
+if [[ "${is_windows}" == "true" ]]; then
+  ${goto_cc} "/c" "/Foproject.gb" --export-file-local-symbols project.c
+  ${goto_cc} "/c" "/Foproof.gb" --export-file-local-symbols proof.c
+  ${goto_cc} "/Fetest.gb" project.gb proof.gb
+else
+  ${goto_cc} -o project.gb --export-file-local-symbols project.c
+  ${goto_cc} -o proof.gb --export-file-local-symbols proof.c
+  ${goto_cc} -o test.gb project.gb proof.gb
+fi

src/goto-analyzer/unreachable_instructions.cpp

@@ -179,10 +179,8 @@ void unreachable_instructions(
 
     const symbolt &decl = ns.lookup(gf_entry.first);
 
-    // gf_entry.first may be a link-time renamed version, use the
-    // base_name instead; do not list inlined functions
     if(
-      called.find(decl.base_name) != called.end() ||
+      called.find(decl.name) != called.end() ||
       to_code_type(decl.type).get_inlined())
     {
       unreachable_instructions(goto_program, dead_map);
@@ -314,10 +312,8 @@ static void list_functions(
   {
     const symbolt &decl = ns.lookup(gf_entry.first);
 
-    // gf_entry.first may be a link-time renamed version, use the
-    // base_name instead; do not list inlined functions
     if(
-      unreachable == (called.find(decl.base_name) != called.end() ||
+      unreachable == (called.find(decl.name) != called.end() ||
                       to_code_type(decl.type).get_inlined()))
     {
       continue;