Allow old --export-function-local-symbols flag

This commit allows users to pass the --export-function-local-symbols
flag, which was deprecated in favour of the less-confusingly named
--export-file-local symbols. This was always the intention, but goto-cc
was erroring out when the old flag was passed. This commit instead
prints out a deprecation warning. This commit includes a test to ensure
that the warning is printed and that goto-cc successfully exports the
local symbols anyway.

Author: karkhaz

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

@@ -47,6 +47,13 @@ if is_in wall "$ALL_ARGS"; then
   fi
 fi
 
+export_flag=""
+if is_in old-flag "$ALL_ARGS"; then
+  export_flag="--export-function-local-symbols"
+else
+  export_flag="--export-file-local-symbols"
+fi
+
 cnt=0
 for src in ${SRC}; do
   cnt=$((cnt + 1))
@@ -63,7 +70,7 @@ for src in ${SRC}; do
 
   if [[ "${is_windows}" == "true" ]]; then
     "${goto_cc}"                        \
-        --export-file-local-symbols \
+        ${export_flag}                  \
         --verbosity 10                  \
         ${wall}                         \
         ${suffix}                       \
@@ -72,7 +79,7 @@ for src in ${SRC}; do
 
   else
     "${goto_cc}"                        \
-        --export-file-local-symbols \
+        ${export_flag}                  \
         --verbosity 10                  \
         ${wall}                         \
         ${suffix}                       \
@@ -86,7 +93,7 @@ if is_in final-link "$ALL_ARGS"; then
   rm -f ${OUT_FILE}
   if [[ "${is_windows}" == "true" ]]; then
     "${goto_cc}"                        \
-        --export-file-local-symbols \
+        ${export_flag}                  \
         --verbosity 10                  \
         ${wall}                         \
         ${suffix}                       \
@@ -95,7 +102,7 @@ if is_in final-link "$ALL_ARGS"; then
 
   else
     "${goto_cc}"                        \
-        --export-file-local-symbols \
+        ${export_flag}                  \
         --verbosity 10                  \
         ${wall}                         \
         ${suffix}                       \

regression/goto-cc-file-local/old-flag-name/foo.c

@@ -0,0 +1,4 @@
+static int foo()
+{
+  return 1;
+}

regression/goto-cc-file-local/old-flag-name/main.c

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

regression/goto-cc-file-local/old-flag-name/test.desc

@@ -0,0 +1,12 @@
+CORE
+main.c
+final-link assertion-check old-flag
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+^The `--export-function-local-symbols` flag is deprecated. Please use `--export-file-local-symbols` instead.$
+--
+^warning: ignoring
+^\*\*\*\* WARNING: no body for function
+--
+Check that goto-cc emits a warning when using the old command line flag

src/goto-cc/gcc_cmdline.cpp

@@ -53,6 +53,8 @@ const char *goto_cc_options_without_argument[]=
   "--validate-goto-model",
   "-?",
   "--export-file-local-symbols",
+  // This is deprecated. Currently prints out a deprecation warning.
+  "--export-function-local-symbols",
   nullptr
 };