export-file-local-symbols: help output and handling of large files

goto-cc --export-file-local-symbols was never documented in --help
output. Its use entails renaming of file-local (function) symbols with a
prefix of __CPROVER_file_local, which had the side effect of those names
being added as defines when building hybrid binaries. For files with
large numbers of static functions, this resulted in a command-line that
exceeds operating-system limits.

Author: tautschnig

src/goto-cc/compile.cpp

@@ -746,6 +746,9 @@ bool compilet::add_written_cprover_symbols(const symbol_tablet &symbol_table)
     if(!(has_prefix(id2string(name), CPROVER_PREFIX) && new_type.id()==ID_code))
       continue;
 
+    if(has_prefix(id2string(name), FILE_LOCAL_PREFIX))
+      continue;
+
     bool inserted;
     std::map<irep_idt, symbolt>::iterator old;
     std::tie(old, inserted)=written_macros.insert({name, pair.second});

src/goto-cc/goto_cc_mode.cpp

@@ -63,6 +63,9 @@ void goto_cc_modet::help()
   " --native-compiler cmd       command to invoke as preprocessor/compiler\n"
   " --native-linker cmd         command to invoke as linker\n"
   " --native-assembler cmd      command to invoke as assembler (goto-as only)\n"
+  " --export-file-local-symbols\n"
+  "                             name-mangle and export file-local symbols\n"
+  " --mangle-suffix suffix      append suffix to exported file-local symbols\n"
   " --print-rejected-preprocessed-source file\n"
   "                             copy failing (preprocessed) source to file\n"
   " --object-bits               number of bits used for object addresses\n"