Allow --export-function-local-symbols mangling for multi-file compilation

Fixes #4689

Author: Christopher Wagner

regression/goto-cc-file-local/chain.sh

@@ -54,39 +54,61 @@ else
   export_flag="--export-file-local-symbols"
 fi
 
-cnt=0
-for src in ${SRC}; do
-  cnt=$((cnt + 1))
-  out_suffix=""
-  if is_in out-file-counter "$ALL_ARGS"; then
-    out_suffix="_$cnt"
-    if is_in suffix "$ALL_ARGS"; then
-      suffix="--mangle-suffix custom_$cnt"
+OUT_FILE="main.gb"
+if is_in compile-and-link "$ALL_ARGS"; then
+    if [[ "${is_windows}" == "true" ]]; then
+      "${goto_cc}"                        \
+          ${export_flag}                  \
+          --verbosity 10                  \
+          ${wall}                         \
+          ${suffix}                       \
+          ${SRC}                          \
+          /Fe"${OUT_FILE}"
+  
+    else
+      "${goto_cc}"                        \
+          ${export_flag}                  \
+          --verbosity 10                  \
+          ${wall}                         \
+          ${suffix}                       \
+          ${SRC}                          \
+          -o "${OUT_FILE}"
     fi
-  fi
-
-  base=${src%.c}
-  OUT_FILE=$(basename "${base}${out_suffix}")".gb"
-
-  if [[ "${is_windows}" == "true" ]]; then
-    "${goto_cc}"                        \
-        ${export_flag}                  \
-        --verbosity 10                  \
-        ${wall}                         \
-        ${suffix}                       \
-        /c "${base}.c"                  \
-        /Fo"${OUT_FILE}"
-
-  else
-    "${goto_cc}"                        \
-        ${export_flag}                  \
-        --verbosity 10                  \
-        ${wall}                         \
-        ${suffix}                       \
-        -c "${base}.c"                  \
-        -o "${OUT_FILE}"
-  fi
-done
+else
+  cnt=0
+  for src in ${SRC}; do
+    cnt=$((cnt + 1))
+    out_suffix=""
+    if is_in out-file-counter "$ALL_ARGS"; then
+      out_suffix="_$cnt"
+      if is_in suffix "$ALL_ARGS"; then
+        suffix="--mangle-suffix custom_$cnt"
+      fi
+    fi
+  
+    base=${src%.c}
+    OUT_FILE=$(basename "${base}${out_suffix}")".gb"
+  
+    if [[ "${is_windows}" == "true" ]]; then
+      "${goto_cc}"                        \
+          ${export_flag}                  \
+          --verbosity 10                  \
+          ${wall}                         \
+          ${suffix}                       \
+          /c "${base}.c"                  \
+          /Fo"${OUT_FILE}"
+  
+    else
+      "${goto_cc}"                        \
+          ${export_flag}                  \
+          --verbosity 10                  \
+          ${wall}                         \
+          ${suffix}                       \
+          -c "${base}.c"                  \
+          -o "${OUT_FILE}"
+    fi
+  done
+fi
 
 if is_in final-link "$ALL_ARGS"; then
   OUT_FILE=final-link.gb

regression/goto-cc-file-local/combined-compile-and-link/foo.c

@@ -0,0 +1,7 @@
+#include <assert.h>
+
+static int foo()
+{
+  assert(0);
+  return 1;
+}

regression/goto-cc-file-local/combined-compile-and-link/main.c

@@ -0,0 +1,6 @@
+int __CPROVER_file_local_foo_c_foo();
+
+int main()
+{
+  return __CPROVER_file_local_foo_c_foo();
+}

regression/goto-cc-file-local/combined-compile-and-link/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+assertion-check compile-and-link
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+^\*\*\*\* WARNING: no body for function
+--
+Check that when files are compiled together in a single invocation
+of goto-cc, exported function symbols are still mangled correctly.

src/goto-cc/compile.cpp

@@ -346,6 +346,13 @@ bool compilet::link()
     convert_symbols(goto_model.goto_functions);
   }
 
+  if(keep_file_local)
+  {
+    function_name_manglert<file_name_manglert> mangler(
+      get_message_handler(), goto_model, file_local_mangle_suffix);
+    mangler.mangle();
+  }
+
   if(write_bin_object_file(output_file_executable, goto_model))
     return true;