Linking: update base name and pretty name of code-typed symbols

Name mangling via --export-file-local-symbols will introduce symbols the
name of which does not match the base name. Forward declarations of the
mangled name, however, do introduce a symbol where (mangled) name and
base name match. When linking later finds the definition corresponding
to such a forward declaration, the base name (and pretty name) need to
be updated. Without these updates, the order of linking would produce
two different final symbol tables.

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\.\.\.: foo$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^Base name\.\.\.: __CPROVER_file_local_.*_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\.\.\.: foo$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^Base name\.\.\.: __CPROVER_file_local_.*_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).

src/linking/linking.cpp

@@ -772,6 +772,8 @@ void linkingt::duplicate_code_symbol(
       // the one with body wins!
       rename_symbol(new_symbol.value);
       rename_symbol(new_symbol.type);
+      old_symbol.base_name = new_symbol.base_name;
+      old_symbol.pretty_name = new_symbol.pretty_name;
       old_symbol.value=new_symbol.value;
       old_symbol.type=new_symbol.type; // for parameter identifiers
       old_symbol.is_weak=new_symbol.is_weak;