Merge pull request #6337 from tautschnig/fix-6330

export-file-local_symbols:: update base name and pretty name

Author: tautschnig

regression/goto-cc-file-local/base-name-1/file1.c

@@ -0,0 +1,7 @@
+int __CPROVER_file_local_file2_c_foo(int x);
+
+int main()
+{
+  int x = __CPROVER_file_local_file2_c_foo(1);
+  __CPROVER_assert(x == 2, "x == 2");
+}

regression/goto-cc-file-local/base-name-1/file2.c

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

regression/goto-cc-file-local/base-name-1/test.desc

@@ -0,0 +1,13 @@
+CORE
+file1.c
+final-link show-symbol-table assertion-check
+^Base name\.\.\.: __CPROVER_file_local_.*_foo$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^Base name\.\.\.: foo$
+--
+The linking order must not affect the base name of the mangled symbol. See
+base-name-2 for a test that will yield a different linking order (while still
+producing the same base name).

regression/goto-cc-file-local/base-name-2/file1.c

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

regression/goto-cc-file-local/base-name-2/file2.c

@@ -0,0 +1,7 @@
+int __CPROVER_file_local_file1_c_foo(int x);
+
+int main()
+{
+  int x = __CPROVER_file_local_file1_c_foo(1);
+  __CPROVER_assert(x == 2, "x == 2");
+}

regression/goto-cc-file-local/base-name-2/test.desc

@@ -0,0 +1,13 @@
+CORE
+file1.c
+final-link show-symbol-table assertion-check
+^Base name\.\.\.: __CPROVER_file_local_.*_foo$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^Base name\.\.\.: foo$
+--
+The linking order must not affect the base name of the mangled symbol. See
+base-name-1 for a test that will yield a different linking order (while still
+producing the same base name).

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

@@ -1,11 +1,10 @@
 CORE
 test.c
 --reachable-functions
-^.* foo 1 4$
+^.* __CPROVER_file_local_project_c_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,

src/goto-programs/name_mangler.h

@@ -70,6 +70,9 @@ class function_name_manglert
       symbolt new_sym;
       new_sym = sym;
       new_sym.name = mangled;
+      new_sym.base_name = mangled;
+      if(new_sym.pretty_name.empty())
+        new_sym.pretty_name = sym.base_name;
       new_sym.is_file_local = false;
 
       new_syms.push_back(new_sym);