diff --git a/doc/architectural/static-functions.md b/doc/architectural/static-functions.md
index 8c38b797675..2c0630ea995 100644
--- a/doc/architectural/static-functions.md
+++ b/doc/architectural/static-functions.md
@@ -92,7 +92,8 @@ We should now also write a harness for `private_function`. However,
 since that function is marked `static`, it is not possible for functions
 in external files to call it. We can write and link a harness by
 stripping the `static` attribute from `private_function` using goto-cc's
-`--export-file-local-symbols` flag.
+`--export-file-local-symbols` or `--export-file-local-symbol private_function`
+flag.
 
 \code{.sh}
 > goto-cc -c -o --export-file-local-symbols library_with_static.o library.c
diff --git a/regression/goto-cc-file-local/chain.sh b/regression/goto-cc-file-local/chain.sh
index 0af9f69e57c..d23de3dad7a 100755
--- a/regression/goto-cc-file-local/chain.sh
+++ b/regression/goto-cc-file-local/chain.sh
@@ -50,6 +50,9 @@ fi
 export_flag=""
 if is_in old-flag "$ALL_ARGS"; then
   export_flag="--export-function-local-symbols"
+elif is_in "export-[a-zA-Z0-9_,]*-only" "$ALL_ARGS"; then
+  names=${ALL_ARGS#*export-}
+  export_flag="--export-file-local-symbol ${names%-only*}"
 else
   export_flag="--export-file-local-symbols"
 fi
diff --git a/regression/goto-cc-file-local/objects/main.c b/regression/goto-cc-file-local/objects/main.c
new file mode 100644
index 00000000000..a570e0a1dd2
--- /dev/null
+++ b/regression/goto-cc-file-local/objects/main.c
@@ -0,0 +1,8 @@
+static int foo = 42;
+
+static int bar = 42;
+
+int baz(int x)
+{
+  return x + 2;
+}
diff --git a/regression/goto-cc-file-local/objects/test.desc b/regression/goto-cc-file-local/objects/test.desc
new file mode 100644
index 00000000000..c4f6b6304e6
--- /dev/null
+++ b/regression/goto-cc-file-local/objects/test.desc
@@ -0,0 +1,11 @@
+CORE
+main.c
+show-symbol-table
+^Symbol\.\.\.\.\.\.: __CPROVER_file_local_main_c_foo$
+^Symbol\.\.\.\.\.\.: __CPROVER_file_local_main_c_bar$
+^Symbol\.\.\.\.\.\.: baz$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^Symbol\.\.\.\.\.\.: __CPROVER_file_local_main_c_baz::x$
diff --git a/regression/goto-cc-file-local/selected-symbols/main.c b/regression/goto-cc-file-local/selected-symbols/main.c
new file mode 100644
index 00000000000..3b1bbd66480
--- /dev/null
+++ b/regression/goto-cc-file-local/selected-symbols/main.c
@@ -0,0 +1,14 @@
+static int foo(int x)
+{
+  return x + 1;
+}
+
+static int bar(int x)
+{
+  return x + 2;
+}
+
+static int baz(int x)
+{
+  return x + 2;
+}
diff --git a/regression/goto-cc-file-local/selected-symbols/test.desc b/regression/goto-cc-file-local/selected-symbols/test.desc
new file mode 100644
index 00000000000..430cf03ba83
--- /dev/null
+++ b/regression/goto-cc-file-local/selected-symbols/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+export-foo,bar-only show-symbol-table
+^Symbol\.\.\.\.\.\.: __CPROVER_file_local_main_c_foo$
+^Symbol\.\.\.\.\.\.: __CPROVER_file_local_main_c_bar$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+^Symbol\.\.\.\.\.\.: __CPROVER_file_local_main_c_baz$
diff --git a/src/ansi-c/ansi_c_language.cpp b/src/ansi-c/ansi_c_language.cpp
index 874539d2402..d29bf00a7c4 100644
--- a/src/ansi-c/ansi_c_language.cpp
+++ b/src/ansi-c/ansi_c_language.cpp
@@ -103,7 +103,7 @@ bool ansi_c_languaget::parse(
 bool ansi_c_languaget::typecheck(
   symbol_tablet &symbol_table,
   const std::string &module,
-  const bool keep_file_local)
+  const std::string &keep_file_local)
 {
   symbol_tablet new_symbol_table;
 
diff --git a/src/ansi-c/ansi_c_language.h b/src/ansi-c/ansi_c_language.h
index 2fa003c521a..3e4a34a36bc 100644
--- a/src/ansi-c/ansi_c_language.h
+++ b/src/ansi-c/ansi_c_language.h
@@ -54,7 +54,7 @@ class ansi_c_languaget:public languaget
   bool typecheck(
     symbol_tablet &symbol_table,
     const std::string &module,
-    const bool keep_file_local) override;
+    const std::string &keep_file_local) override;
 
   bool can_keep_file_local() override
   {
@@ -64,7 +64,7 @@ class ansi_c_languaget:public languaget
   bool
   typecheck(symbol_tablet &symbol_table, const std::string &module) override
   {
-    return typecheck(symbol_table, module, true);
+    return typecheck(symbol_table, module, ".*");
   }
 
   void show_parse(std::ostream &out) override;
diff --git a/src/cpp/cpp_language.cpp b/src/cpp/cpp_language.cpp
index 93513163b96..171cdea2f38 100644
--- a/src/cpp/cpp_language.cpp
+++ b/src/cpp/cpp_language.cpp
@@ -131,7 +131,7 @@ bool cpp_languaget::typecheck(
       cpp_parse_tree, new_symbol_table, module, get_message_handler()))
     return true;
 
-  remove_internal_symbols(new_symbol_table, get_message_handler(), false);
+  remove_internal_symbols(new_symbol_table, get_message_handler(), "");
 
   return linking(symbol_table, new_symbol_table, get_message_handler());
 }
diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp
index 8da13587f34..daf28e35bd3 100644
--- a/src/goto-cc/compile.cpp
+++ b/src/goto-cc/compile.cpp
@@ -23,6 +23,7 @@ Date: June 2006
 #include <util/get_base_name.h>
 #include <util/prefix.h>
 #include <util/run.h>
+#include <util/string_utils.h>
 #include <util/symbol_table_builder.h>
 #include <util/tempdir.h>
 #include <util/tempfile.h>
@@ -353,10 +354,13 @@ bool compilet::link(optionalt<symbol_tablet> &&symbol_table)
     convert_symbols(goto_model);
   }
 
-  if(keep_file_local)
+  if(!keep_file_local.empty())
   {
-    function_name_manglert<file_name_manglert> mangler(
-      log.get_message_handler(), goto_model, file_local_mangle_suffix);
+    file_local_name_manglert<file_name_manglert> mangler(
+      log.get_message_handler(),
+      goto_model,
+      file_local_mangle_suffix,
+      keep_file_local);
     mangler.mangle();
   }
 
@@ -424,10 +428,13 @@ optionalt<symbol_tablet> compilet::compile()
       else
         cfn = output_file_object;
 
-      if(keep_file_local)
+      if(!keep_file_local.empty())
       {
-        function_name_manglert<file_name_manglert> mangler(
-          log.get_message_handler(), file_goto_model, file_local_mangle_suffix);
+        file_local_name_manglert<file_name_manglert> mangler(
+          log.get_message_handler(),
+          file_goto_model,
+          file_local_mangle_suffix,
+          keep_file_local);
         mangler.mangle();
       }
 
@@ -645,6 +652,27 @@ optionalt<symbol_tablet> compilet::parse_source(const std::string &file_name)
   return std::move(file_symbol_table);
 }
 
+/// Combine the elements of \p values to a regular expression denoting
+/// alternatives. Each element of \p values may in turn be a sequence of
+/// comma-separated values, which are also expanded to contribute to the overall
+/// collection of alternatives.
+static std::string csv_to_pattern(const std::list<std::string> &values)
+{
+  std::string result;
+
+  for(const auto &csv : values)
+  {
+    for(const auto &name : split_string(csv, ','))
+    {
+      if(!result.empty())
+        result += '|';
+      result += name;
+    }
+  }
+
+  return result;
+}
+
 /// constructor
 compilet::compilet(cmdlinet &_cmdline, message_handlert &mh, bool Werror)
   : log(mh),
@@ -652,8 +680,12 @@ compilet::compilet(cmdlinet &_cmdline, message_handlert &mh, bool Werror)
     warning_is_fatal(Werror),
     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")),
+      (cmdline.isset("export-function-local-symbols") ||
+       cmdline.isset("export-file-local-symbols"))
+        ? ".*"
+        : (cmdline.isset("export-file-local-symbol")
+             ? csv_to_pattern(cmdline.get_values("export-file-local-symbol"))
+             : "")),
     file_local_mangle_suffix(
       cmdline.isset("mangle-suffix") ? cmdline.get_value("mangle-suffix") : "")
 {
diff --git a/src/goto-cc/compile.h b/src/goto-cc/compile.h
index f8480649a48..2eb0e09c850 100644
--- a/src/goto-cc/compile.h
+++ b/src/goto-cc/compile.h
@@ -111,7 +111,7 @@ class compilet
   bool warning_is_fatal;
 
   /// \brief Whether to keep implementations of file-local symbols
-  const bool keep_file_local;
+  const std::string keep_file_local;
 
   /// \brief String to include in all mangled names
   const std::string file_local_mangle_suffix;
diff --git a/src/goto-cc/gcc_cmdline.cpp b/src/goto-cc/gcc_cmdline.cpp
index 0e91dc1b3d6..4bf52232b8d 100644
--- a/src/goto-cc/gcc_cmdline.cpp
+++ b/src/goto-cc/gcc_cmdline.cpp
@@ -28,6 +28,7 @@ const char *goto_cc_options_with_separated_argument[]=
   "--print-rejected-preprocessed-source",
   "--mangle-suffix",
   "--object-bits",
+  "--export-file-local-symbol",
   nullptr
 };
 
diff --git a/src/goto-cc/goto_cc_mode.cpp b/src/goto-cc/goto_cc_mode.cpp
index 1f38388619b..43e2aa652fb 100644
--- a/src/goto-cc/goto_cc_mode.cpp
+++ b/src/goto-cc/goto_cc_mode.cpp
@@ -64,6 +64,12 @@ 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"
+  " --export-file-local-symbol A,B\n"
+  "                             export file-local symbols as above, but\n"
+  "                             restrict this operation to symbols A and B\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"
diff --git a/src/goto-cc/ms_cl_cmdline.cpp b/src/goto-cc/ms_cl_cmdline.cpp
index d8291a43fdd..705e6ed164b 100644
--- a/src/goto-cc/ms_cl_cmdline.cpp
+++ b/src/goto-cc/ms_cl_cmdline.cpp
@@ -47,6 +47,7 @@ const char *non_ms_cl_options[]=
   "--validate-goto-model",
   "--export-file-local-symbols",
   "--mangle-suffix",
+  "--export-file-local-symbol",
   nullptr
 };
 // clang-format on
@@ -62,7 +63,8 @@ bool ms_cl_cmdlinet::parse(const std::vector<std::string> &arguments)
 
       if(
         arguments[i] == "--verbosity" || arguments[i] == "--function" ||
-        arguments[i] == "--mangle-suffix")
+        arguments[i] == "--mangle-suffix" ||
+        arguments[i] == "--export-file-local-symbol")
       {
         if(i < arguments.size() - 1)
         {
diff --git a/src/goto-programs/name_mangler.h b/src/goto-programs/name_mangler.h
index 0f3e5a1e5dd..6afa4e28cbf 100644
--- a/src/goto-programs/name_mangler.h
+++ b/src/goto-programs/name_mangler.h
@@ -27,21 +27,28 @@
 /// mangled name of its \ref symbolt argument, incorporating the second
 /// argument into the mangled name if possible.
 template <class MangleFun>
-class function_name_manglert
+class file_local_name_manglert
 {
 public:
   /// \param mh: handler to construct a log from
-  /// \param gm: mangle all names in gm's symbol table and goto program
+  /// \param gm: mangle names in gm's symbol table and goto program
   /// \param extra_info: a string to be included in each mangled name
-  function_name_manglert(
+  /// \param needs_mangling: a regular expression describing names that need to
+  ///   be mangled.
+  file_local_name_manglert(
     message_handlert &mh,
     goto_modelt &gm,
-    const std::string &extra_info)
-    : log(mh), model(gm), mangle_fun(), extra_info(extra_info)
+    const std::string &extra_info,
+    const std::string &needs_mangling)
+    : log(mh),
+      model(gm),
+      mangle_fun(),
+      extra_info(extra_info),
+      needs_mangling(needs_mangling)
   {
   }
 
-  /// \brief Mangle all file-local function symbols in the program
+  /// \brief Mangle all file-local non-type global-scoped symbols in the program
   ///
   /// The way in which the symbols will be mangled is decided by which mangler
   /// type this object is instantiated with, e.g. DJB_manglert mangles the path
@@ -59,11 +66,16 @@ class function_name_manglert
     {
       const symbolt &sym = sym_it->second;
 
-      if(sym.type.id() != ID_code) // is not a function
+      if(!sym.is_file_local)
         continue;
-      if(sym.value.is_nil()) // has no body
+      if(sym.is_type)
         continue;
-      if(!sym.is_file_local)
+      // no name mangling for functions without body
+      if(sym.type.id() == ID_code && sym.value.is_nil())
+        continue;
+      if(sym.type.id() != ID_code && !sym.is_static_lifetime)
+        continue;
+      if(!std::regex_match(id2string(sym.name), needs_mangling))
         continue;
 
       const irep_idt mangled = mangle_fun(sym, extra_info);
@@ -76,7 +88,8 @@ class function_name_manglert
       old_syms.push_back(sym_it);
 
       rename.insert(sym.symbol_expr(), new_sym.symbol_expr());
-      renamed_funs.insert(std::make_pair(sym.name, mangled));
+      if(sym.type.id() == ID_code)
+        renamed_funs.insert(std::make_pair(sym.name, mangled));
 
       log.debug() << "Mangling: " << sym.name << " -> " << mangled << log.eom;
     }
@@ -136,6 +149,7 @@ class function_name_manglert
   goto_modelt &model;
   MangleFun mangle_fun;
   const std::string &extra_info;
+  const std::regex needs_mangling;
 };
 
 /// \brief Mangle identifiers by including their filename
diff --git a/src/langapi/language.h b/src/langapi/language.h
index a33304d941c..74458b9f71e 100644
--- a/src/langapi/language.h
+++ b/src/langapi/language.h
@@ -140,7 +140,7 @@ class languaget:public messaget
   virtual bool typecheck(
     symbol_tablet &symbol_table,
     const std::string &module,
-    const bool keep_file_local)
+    const std::string &keep_file_local)
   {
     INVARIANT(
       false,
diff --git a/src/langapi/language_file.cpp b/src/langapi/language_file.cpp
index 440d682a9d8..bed254d0b36 100644
--- a/src/langapi/language_file.cpp
+++ b/src/langapi/language_file.cpp
@@ -82,7 +82,7 @@ bool language_filest::parse()
 
 bool language_filest::typecheck(
   symbol_tablet &symbol_table,
-  const bool keep_file_local)
+  const std::string &keep_file_local)
 {
   // typecheck interfaces
 
@@ -204,7 +204,7 @@ bool language_filest::interfaces(
 bool language_filest::typecheck_module(
   symbol_tablet &symbol_table,
   const std::string &module,
-  const bool keep_file_local)
+  const std::string &keep_file_local)
 {
   // check module map
 
@@ -222,7 +222,7 @@ bool language_filest::typecheck_module(
 bool language_filest::typecheck_module(
   symbol_tablet &symbol_table,
   language_modulet &module,
-  const bool keep_file_local)
+  const std::string &keep_file_local)
 {
   // already typechecked?
 
diff --git a/src/langapi/language_file.h b/src/langapi/language_file.h
index 4aa9f9a1a25..0be4dcb21bf 100644
--- a/src/langapi/language_file.h
+++ b/src/langapi/language_file.h
@@ -108,8 +108,9 @@ class language_filest:public messaget
 
   bool generate_support_functions(symbol_tablet &symbol_table);
 
-  bool
-  typecheck(symbol_tablet &symbol_table, const bool keep_file_local = false);
+  bool typecheck(
+    symbol_tablet &symbol_table,
+    const std::string &keep_file_local = "");
 
   bool final(symbol_table_baset &symbol_table);
 
@@ -144,12 +145,12 @@ class language_filest:public messaget
   bool typecheck_module(
     symbol_tablet &symbol_table,
     language_modulet &module,
-    const bool keep_file_local);
+    const std::string &keep_file_local);
 
   bool typecheck_module(
     symbol_tablet &symbol_table,
     const std::string &module,
-    const bool keep_file_local);
+    const std::string &keep_file_local);
 };
 
 #endif // CPROVER_UTIL_LANGUAGE_FILE_H
diff --git a/src/linking/remove_internal_symbols.cpp b/src/linking/remove_internal_symbols.cpp
index 9a7d69aa509..ce7c5d6b487 100644
--- a/src/linking/remove_internal_symbols.cpp
+++ b/src/linking/remove_internal_symbols.cpp
@@ -22,6 +22,8 @@ Author: Daniel Kroening
 
 #include "static_lifetime_init.h"
 
+#include <regex>
+
 static void get_symbols(
   const namespacet &ns,
   const symbolt &in_symbol,
@@ -99,12 +101,12 @@ static void get_symbols(
 ///          on "extern inline"
 /// \param symbol_table: symbol table to clean up
 /// \param mh: log handler
-/// \param keep_file_local: keep file-local functions with bodies even if we
+/// \param keep_file_local: regular expression over symbols to keep even if we
 ///                         would otherwise remove them
 void remove_internal_symbols(
   symbol_tablet &symbol_table,
   message_handlert &mh,
-  const bool keep_file_local)
+  const std::string &keep_file_local)
 {
   namespacet ns(symbol_table);
   find_symbols_sett exported;
@@ -176,7 +178,9 @@ void remove_internal_symbols(
       {
         get_symbols(ns, symbol, exported);
       }
-      else if(has_body && is_file_local && keep_file_local)
+      else if(
+        has_body && is_file_local && !keep_file_local.empty() &&
+        std::regex_match(id2string(symbol.name), std::regex(keep_file_local)))
       {
         get_symbols(ns, symbol, exported);
       }
@@ -185,8 +189,12 @@ void remove_internal_symbols(
     {
       // 'extern' symbols are only exported if there
       // is an initializer.
-      if((has_initializer || !symbol.is_extern) &&
-         !is_file_local)
+      if(
+        (has_initializer || !symbol.is_extern) &&
+        (!is_file_local ||
+         (symbol.is_static_lifetime && !keep_file_local.empty() &&
+          std::regex_match(
+            id2string(symbol.name), std::regex(keep_file_local)))))
       {
         get_symbols(ns, symbol, exported);
       }
diff --git a/src/linking/remove_internal_symbols.h b/src/linking/remove_internal_symbols.h
index 18446a9223b..13c62f1fff0 100644
--- a/src/linking/remove_internal_symbols.h
+++ b/src/linking/remove_internal_symbols.h
@@ -12,11 +12,13 @@ Author: Daniel Kroening
 #ifndef CPROVER_LINKING_REMOVE_INTERNAL_SYMBOLS_H
 #define CPROVER_LINKING_REMOVE_INTERNAL_SYMBOLS_H
 
+#include <string>
+
 class message_handlert;
 
 void remove_internal_symbols(
   class symbol_tablet &symbol_table,
   message_handlert &,
-  const bool);
+  const std::string &);
 
 #endif // CPROVER_LINKING_REMOVE_INTERNAL_SYMBOLS_H
diff --git a/src/statement-list/statement_list_language.cpp b/src/statement-list/statement_list_language.cpp
index f7e2c8f85f0..865c1f96c59 100644
--- a/src/statement-list/statement_list_language.cpp
+++ b/src/statement-list/statement_list_language.cpp
@@ -36,7 +36,7 @@ bool statement_list_languaget::generate_support_functions(
 bool statement_list_languaget::typecheck(
   symbol_tablet &symbol_table,
   const std::string &module,
-  const bool keep_file_local)
+  const std::string &keep_file_local)
 {
   symbol_tablet new_symbol_table;
 
@@ -85,7 +85,7 @@ bool statement_list_languaget::typecheck(
   symbol_tablet &symbol_table,
   const std::string &module)
 {
-  return typecheck(symbol_table, module, true);
+  return typecheck(symbol_table, module, ".*");
 }
 
 bool statement_list_languaget::from_expr(
diff --git a/src/statement-list/statement_list_language.h b/src/statement-list/statement_list_language.h
index 6edc0cdda42..e31ba0abe2d 100644
--- a/src/statement-list/statement_list_language.h
+++ b/src/statement-list/statement_list_language.h
@@ -43,13 +43,14 @@ class statement_list_languaget : public languaget
   ///   If the symbol table is not empty when calling this function, its
   ///   contents are merged with the new entries.
   /// \param module: Name of the file that has been parsed.
-  /// \param keep_file_local: Set to true if local variables of this module
-  ///   should be included in the table.
+  /// \param keep_file_local: Set to non-empty string that is used as regular
+  ///   expression over local variable names that must not be cleaned from the
+  ///   symbol table.
   /// \return False if no errors occurred, true otherwise.
   bool typecheck(
     symbol_tablet &symbol_table,
     const std::string &module,
-    const bool keep_file_local) override;
+    const std::string &keep_file_local) override;
 
   bool
   typecheck(symbol_tablet &symbol_table, const std::string &module) override;