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

Name mangling via --export-file-local-symbols used to introduce symbols
the name of which did not match the base name. Forward declarations of
the mangled name, however, did introduce a symbol where (mangled) name
and base name match. When linking later found the definition
corresponding to such a forward declaration, the base name (and pretty
name) were not updated. As a consequence the order of linking produced
two different final symbol tables.

Note that Crangler may be a superior alternative avoiding such problems,
but there is ample code that still uses `--export-file-local-symbols`.

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);