Change goto-cc function-local to file-local

goto-cc had a misleading flag called `--export-function-local-symbols`.
This flag exported the declarations of all static functions in a file,
and is thus more appropriately named `--export-file-local-symbols`. That
was actually the flag's old name, and indeed those functions' mangled
name would be prefixed with `__CPROVER_file_local`. Some of the
documentation also referred to the flag's old name.

This commit makes the documentation and flags consistent with the
internal implementation, i.e. the flag is now called
`--export-file-local-symbols`. The `function` flag is still accepted
because some existing code in the wild relies on this, but goto-cc emits
a warning if the user passes that flag.

Author: karkhaz

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

@@ -63,7 +63,7 @@ for src in ${SRC}; do
 
   if [[ "${is_windows}" == "true" ]]; then
     "${goto_cc}"                        \
-        --export-function-local-symbols \
+        --export-file-local-symbols \
         --verbosity 10                  \
         ${wall}                         \
         ${suffix}                       \
@@ -72,7 +72,7 @@ for src in ${SRC}; do
 
   else
     "${goto_cc}"                        \
-        --export-function-local-symbols \
+        --export-file-local-symbols \
         --verbosity 10                  \
         ${wall}                         \
         ${suffix}                       \
@@ -86,7 +86,7 @@ if is_in final-link "$ALL_ARGS"; then
   rm -f ${OUT_FILE}
   if [[ "${is_windows}" == "true" ]]; then
     "${goto_cc}"                        \
-        --export-function-local-symbols \
+        --export-file-local-symbols \
         --verbosity 10                  \
         ${wall}                         \
         ${suffix}                       \
@@ -95,7 +95,7 @@ if is_in final-link "$ALL_ARGS"; then
 
   else
     "${goto_cc}"                        \
-        --export-function-local-symbols \
+        --export-file-local-symbols \
         --verbosity 10                  \
         ${wall}                         \
         ${suffix}                       \

src/goto-cc/compile.cpp

@@ -626,14 +626,21 @@ compilet::compilet(cmdlinet &_cmdline, message_handlert &mh, bool Werror)
     ns(goto_model.symbol_table),
     cmdline(_cmdline),
     warning_is_fatal(Werror),
-    keep_file_local(cmdline.isset("export-function-local-symbols")),
+    keep_file_local(
+        // function-local is the old name and is still in use, but is misleading
+        cmdline.isset("export-function-local-symbols") ||
+        cmdline.isset("export-file-local-symbols")),
     file_local_mangle_suffix(
       cmdline.isset("mangle-suffix") ? cmdline.get_value("mangle-suffix") : "")
 {
   mode=COMPILE_LINK_EXECUTABLE;
   echo_file_name=false;
   wrote_object=false;
   working_directory=get_current_working_directory();
+
+  if(cmdline.isset("export-function-local-symbols"))
+    warning() << "The `--export-function-local-symbols` flag is deprecated. "
+                 "Please use `--export-file-local-symbols` instead." << eom;
 }
 
 /// cleans up temporary files

src/goto-cc/gcc_cmdline.cpp

@@ -52,7 +52,7 @@ const char *goto_cc_options_without_argument[]=
   "--partial-inlining",
   "--validate-goto-model",
   "-?",
-  "--export-function-local-symbols",
+  "--export-file-local-symbols",
   nullptr
 };
 

src/goto-cc/ms_cl_cmdline.cpp

@@ -46,7 +46,7 @@ const char *non_ms_cl_options[]=
   "--verbosity",
   "--function",
   "--validate-goto-model",
-  "--export-function-local-symbols",
+  "--export-file-local-symbols",
   "--mangle-suffix",
   nullptr
 };