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

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}                       \