Add docs for --export-file-local-symbols

Author: karkhaz

doc/architectural/static-functions.md

@@ -59,7 +59,9 @@ For performance reasons, it might be desirable to analyze the API
 function independently of the static function. We can analyze the API
 function by "stubbing out" the static function, replacing it with a
 function that does nothing apart from asserting that its inputs satisfy
-the function's contract. Add the following to `harness.c`:
+the function's contract. ("Stubbing out" a function is sometimes known
+as "modelling" or "abstracting it out".) Add the following to
+`harness.c`:
 
 \code{.c}
 static void private_function(const int *a, int *b)

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,22 @@ 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
 };