diff --git a/regression/goto-cc-cbmc/mixed-c-library-goto-main/lib.c b/regression/goto-cc-cbmc/mixed-c-library-goto-main/lib.c
new file mode 100644
index 00000000000..a8a5b43ccda
--- /dev/null
+++ b/regression/goto-cc-cbmc/mixed-c-library-goto-main/lib.c
@@ -0,0 +1,4 @@
+
+int getone() {
+  return 1;
+}
diff --git a/regression/goto-cc-cbmc/mixed-c-library-goto-main/main.c b/regression/goto-cc-cbmc/mixed-c-library-goto-main/main.c
new file mode 100644
index 00000000000..477a2849bc4
--- /dev/null
+++ b/regression/goto-cc-cbmc/mixed-c-library-goto-main/main.c
@@ -0,0 +1,12 @@
+
+extern int getone();
+
+#include <assert.h>
+
+int main(int argc, char** argv) {
+  assert(getone()==1);
+}
+
+int altmain() {
+  assert(getone()==0);
+}
diff --git a/regression/goto-cc-cbmc/mixed-c-library-goto-main/with_function.desc b/regression/goto-cc-cbmc/mixed-c-library-goto-main/with_function.desc
new file mode 100644
index 00000000000..02a614cf9c2
--- /dev/null
+++ b/regression/goto-cc-cbmc/mixed-c-library-goto-main/with_function.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+lib.c --function altmain
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
diff --git a/regression/goto-cc-cbmc/mixed-c-library-goto-main/without_function.desc b/regression/goto-cc-cbmc/mixed-c-library-goto-main/without_function.desc
new file mode 100644
index 00000000000..223981ebd3d
--- /dev/null
+++ b/regression/goto-cc-cbmc/mixed-c-library-goto-main/without_function.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+lib.c
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/goto-cc-cbmc/mixed-goto-library-c-main/lib.c b/regression/goto-cc-cbmc/mixed-goto-library-c-main/lib.c
new file mode 100644
index 00000000000..a8a5b43ccda
--- /dev/null
+++ b/regression/goto-cc-cbmc/mixed-goto-library-c-main/lib.c
@@ -0,0 +1,4 @@
+
+int getone() {
+  return 1;
+}
diff --git a/regression/goto-cc-cbmc/mixed-goto-library-c-main/main.c b/regression/goto-cc-cbmc/mixed-goto-library-c-main/main.c
new file mode 100644
index 00000000000..477a2849bc4
--- /dev/null
+++ b/regression/goto-cc-cbmc/mixed-goto-library-c-main/main.c
@@ -0,0 +1,12 @@
+
+extern int getone();
+
+#include <assert.h>
+
+int main(int argc, char** argv) {
+  assert(getone()==1);
+}
+
+int altmain() {
+  assert(getone()==0);
+}
diff --git a/regression/goto-cc-cbmc/mixed-goto-library-c-main/with_function.desc b/regression/goto-cc-cbmc/mixed-goto-library-c-main/with_function.desc
new file mode 100644
index 00000000000..02a614cf9c2
--- /dev/null
+++ b/regression/goto-cc-cbmc/mixed-goto-library-c-main/with_function.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+lib.c --function altmain
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
diff --git a/regression/goto-cc-cbmc/mixed-goto-library-c-main/without_function.desc b/regression/goto-cc-cbmc/mixed-goto-library-c-main/without_function.desc
new file mode 100644
index 00000000000..223981ebd3d
--- /dev/null
+++ b/regression/goto-cc-cbmc/mixed-goto-library-c-main/without_function.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+lib.c
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/src/ansi-c/ansi_c_language.cpp b/src/ansi-c/ansi_c_language.cpp
index 19696264996..bbb1236e9e7 100644
--- a/src/ansi-c/ansi_c_language.cpp
+++ b/src/ansi-c/ansi_c_language.cpp
@@ -36,22 +36,6 @@ void ansi_c_languaget::modules_provided(std::set<std::string> &modules)
   modules.insert(get_base_name(parse_path, true));
 }
 
-/// Generate a _start function for a specific function
-/// \param entry_function_symbol_id: The symbol for the function that should be
-///   used as the entry point
-/// \param symbol_table: The symbol table for the program. The new _start
-///   function symbol will be added to this table
-/// \return Returns false if the _start method was generated correctly
-bool ansi_c_languaget::generate_start_function(
-  const irep_idt &entry_function_symbol_id,
-  symbol_tablet &symbol_table)
-{
-  return generate_ansi_c_start_function(
-    symbol_table.symbols.at(entry_function_symbol_id),
-    symbol_table,
-    *message_handler);
-}
-
 /// ANSI-C preprocessing
 bool ansi_c_languaget::preprocess(
   std::istream &instream,
@@ -140,13 +124,19 @@ bool ansi_c_languaget::typecheck(
   return false;
 }
 
-bool ansi_c_languaget::final(symbol_tablet &symbol_table)
+bool ansi_c_languaget::generate_support_functions(
+  symbol_tablet &symbol_table)
 {
+  // Note this can happen here because C doesn't currently
+  // support lazy loading at the symbol-table level, and therefore
+  // function bodies have already been populated and external stub
+  // symbols created during the typecheck() phase. If it gains lazy
+  // loading support then stubs will need to be created during
+  // function body parsing, or else generate-stubs moved to the
+  // final phase.
   generate_opaque_method_stubs(symbol_table);
-  if(ansi_c_entry_point(symbol_table, get_message_handler()))
-    return true;
-
-  return false;
+  // This creates __CPROVER_start and __CPROVER_initialize:
+  return ansi_c_entry_point(symbol_table, get_message_handler());
 }
 
 void ansi_c_languaget::show_parse(std::ostream &out)
diff --git a/src/ansi-c/ansi_c_language.h b/src/ansi-c/ansi_c_language.h
index b86499954c2..78119020c97 100644
--- a/src/ansi-c/ansi_c_language.h
+++ b/src/ansi-c/ansi_c_language.h
@@ -31,13 +31,13 @@ class ansi_c_languaget:public languaget
     std::istream &instream,
     const std::string &path) override;
 
+  bool generate_support_functions(
+    symbol_tablet &symbol_table) override;
+
   bool typecheck(
     symbol_tablet &symbol_table,
     const std::string &module) override;
 
-  bool final(
-    symbol_tablet &symbol_table) override;
-
   void show_parse(std::ostream &out) override;
 
   ~ansi_c_languaget() override;
@@ -73,10 +73,6 @@ class ansi_c_languaget:public languaget
 
   void modules_provided(std::set<std::string> &modules) override;
 
-  virtual bool generate_start_function(
-    const irep_idt &entry_function_symbol_id,
-    class symbol_tablet &symbol_table) override;
-
 protected:
   ansi_c_parse_treet parse_tree;
   std::string parse_path;
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index 2db6b7419f2..b9da1f18c1c 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -52,7 +52,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-programs/show_properties.h>
 #include <goto-programs/string_abstraction.h>
 #include <goto-programs/string_instrumentation.h>
-#include <goto-programs/rebuild_goto_start_function.h>
 
 #include <goto-symex/rewrite_union.h>
 #include <goto-symex/adjust_float_expressions.h>
@@ -630,21 +629,6 @@ int cbmc_parse_optionst::get_goto_program(
     // are already compiled
       return 6;
 
-    if(cmdline.isset("function"))
-    {
-      const std::string &function_id=cmdline.get_value("function");
-      rebuild_goto_start_functiont start_function_rebuilder(
-          get_message_handler(),
-          cmdline,
-          goto_model.symbol_table,
-          goto_model.goto_functions);
-
-      if(start_function_rebuilder(function_id))
-      {
-        return 6;
-      }
-    }
-
     if(cmdline.isset("show-symbol-table"))
     {
       show_symbol_table(goto_model, ui_message_handler.get_ui());
diff --git a/src/cbmc/cbmc_parse_options.h b/src/cbmc/cbmc_parse_options.h
index 08a0ef619ab..7ce7e05dc9f 100644
--- a/src/cbmc/cbmc_parse_options.h
+++ b/src/cbmc/cbmc_parse_options.h
@@ -14,7 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/ui_message.h>
 #include <util/parse_options.h>
-#include <goto-programs/rebuild_goto_start_function.h>
+#include <util/language.h>
 
 #include <analyses/goto_check.h>
 
diff --git a/src/cpp/cpp_language.cpp b/src/cpp/cpp_language.cpp
index f329e9986c0..e47d887d292 100644
--- a/src/cpp/cpp_language.cpp
+++ b/src/cpp/cpp_language.cpp
@@ -53,22 +53,6 @@ void cpp_languaget::modules_provided(std::set<std::string> &modules)
   modules.insert(get_base_name(parse_path, true));
 }
 
-/// Generate a _start function for a specific function
-/// \param entry_function_symbol_id: The symbol for the function that should be
-///   used as the entry point
-/// \param symbol_table: The symbol table for the program. The new _start
-///   function symbol will be added to this table
-/// \return Returns false if the _start method was generated correctly
-bool cpp_languaget::generate_start_function(
-  const irep_idt &entry_function_symbol_id,
-  symbol_tablet &symbol_table)
-{
-  return generate_ansi_c_start_function(
-    symbol_table.lookup(entry_function_symbol_id),
-    symbol_table,
-    *message_handler);
-}
-
 /// ANSI-C preprocessing
 bool cpp_languaget::preprocess(
   std::istream &instream,
@@ -150,12 +134,10 @@ bool cpp_languaget::typecheck(
   return linking(symbol_table, new_symbol_table, get_message_handler());
 }
 
-bool cpp_languaget::final(symbol_tablet &symbol_table)
+bool cpp_languaget::generate_support_functions(
+  symbol_tablet &symbol_table)
 {
-  if(ansi_c_entry_point(symbol_table, get_message_handler()))
-    return true;
-
-  return false;
+  return ansi_c_entry_point(symbol_table, get_message_handler());
 }
 
 void cpp_languaget::show_parse(std::ostream &out)
diff --git a/src/cpp/cpp_language.h b/src/cpp/cpp_language.h
index 36093b8ba8a..fcfbaa38299 100644
--- a/src/cpp/cpp_language.h
+++ b/src/cpp/cpp_language.h
@@ -33,6 +33,9 @@ class cpp_languaget:public languaget
     std::istream &instream,
     const std::string &path) override;
 
+  bool generate_support_functions(
+    symbol_tablet &symbol_table) override;
+
   bool typecheck(
     symbol_tablet &symbol_table,
     const std::string &module) override;
@@ -43,9 +46,6 @@ class cpp_languaget:public languaget
     const std::string &module,
     class replace_symbolt &replace_symbol) const;
 
-  bool final(
-    symbol_tablet &symbol_table) override;
-
   void show_parse(std::ostream &out) override;
 
   // constructor, destructor
@@ -85,10 +85,6 @@ class cpp_languaget:public languaget
 
   void modules_provided(std::set<std::string> &modules) override;
 
-  virtual bool generate_start_function(
-    const irep_idt &entry_function_symbol_id,
-    class symbol_tablet &symbol_table) override;
-
 protected:
   cpp_parse_treet cpp_parse_tree;
   std::string parse_path;
diff --git a/src/goto-analyzer/goto_analyzer_parse_options.h b/src/goto-analyzer/goto_analyzer_parse_options.h
index 62a5932cdb2..4b8f494d402 100644
--- a/src/goto-analyzer/goto_analyzer_parse_options.h
+++ b/src/goto-analyzer/goto_analyzer_parse_options.h
@@ -14,10 +14,10 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/ui_message.h>
 #include <util/parse_options.h>
+#include <util/language.h>
 
 #include <goto-programs/goto_model.h>
 #include <goto-programs/show_goto_functions.h>
-#include <goto-programs/rebuild_goto_start_function.h>
 
 #include <analyses/goto_check.h>
 
diff --git a/src/goto-programs/initialize_goto_model.cpp b/src/goto-programs/initialize_goto_model.cpp
index 4d09607a0b5..96e97493afd 100644
--- a/src/goto-programs/initialize_goto_model.cpp
+++ b/src/goto-programs/initialize_goto_model.cpp
@@ -53,12 +53,11 @@ bool initialize_goto_model(
         sources.push_back(file);
     }
 
+    language_filest language_files;
+    language_files.set_message_handler(message_handler);
+
     if(!sources.empty())
     {
-      language_filest language_files;
-
-      language_files.set_message_handler(message_handler);
-
       for(const auto &filename : sources)
       {
         #ifdef _MSC_VER
@@ -114,19 +113,6 @@ bool initialize_goto_model(
         msg.error() << "CONVERSION ERROR" << messaget::eom;
         return true;
       }
-
-      if(binaries.empty())
-      {
-        // Enable/disable stub generation for opaque methods
-        bool stubs_enabled=cmdline.isset("generate-opaque-stubs");
-        language_files.set_should_generate_opaque_method_stubs(stubs_enabled);
-
-        if(language_files.final(goto_model.symbol_table))
-        {
-          msg.error() << "CONVERSION ERROR" << messaget::eom;
-          return true;
-        }
-      }
     }
 
     for(const auto &file : binaries)
@@ -137,17 +123,49 @@ bool initialize_goto_model(
         return true;
     }
 
-    if(cmdline.isset("function"))
+    bool binaries_provided_start=
+      goto_model.symbol_table.has_symbol(goto_functionst::entry_point());
+
+    bool entry_point_generation_failed=false;
+
+    if(binaries_provided_start && cmdline.isset("function"))
     {
-      const std::string &function_id=cmdline.get_value("function");
-      rebuild_goto_start_functiont start_function_rebuilder(
+      // Rebuild the entry-point, using the language annotation of the
+      // existing __CPROVER_start function:
+      rebuild_goto_start_functiont rebuild_existing_start(
         msg.get_message_handler(),
         cmdline,
         goto_model.symbol_table,
         goto_model.goto_functions);
+      entry_point_generation_failed=rebuild_existing_start();
+    }
+    else if(!binaries_provided_start)
+    {
+      // Unsure of the rationale for only generating stubs when there are no
+      // GOTO binaries in play; simply mirroring old code in language_uit here.
+      if(binaries.empty())
+      {
+        // Enable/disable stub generation for opaque methods
+        bool stubs_enabled=cmdline.isset("generate-opaque-stubs");
+        language_files.set_should_generate_opaque_method_stubs(stubs_enabled);
+      }
 
-      if(start_function_rebuilder(function_id))
-        return true;
+      // Allow all language front-ends to try to provide the user-specified
+      // (--function) entry-point, or some language-specific default:
+      entry_point_generation_failed=
+        language_files.generate_support_functions(goto_model.symbol_table);
+    }
+
+    if(entry_point_generation_failed)
+    {
+      msg.error() << "SUPPORT FUNCTION GENERATION ERROR" << messaget::eom;
+      return true;
+    }
+
+    if(language_files.final(goto_model.symbol_table))
+    {
+      msg.error() << "FINAL STAGE CONVERSION ERROR" << messaget::eom;
+      return true;
     }
 
     msg.status() << "Generating GOTO Program" << messaget::eom;
diff --git a/src/goto-programs/rebuild_goto_start_function.cpp b/src/goto-programs/rebuild_goto_start_function.cpp
index cb4d9e01f3d..76f0deacc2e 100644
--- a/src/goto-programs/rebuild_goto_start_function.cpp
+++ b/src/goto-programs/rebuild_goto_start_function.cpp
@@ -44,8 +44,7 @@ rebuild_goto_start_functiont::rebuild_goto_start_functiont(
 /// called from _start
 /// \return Returns true if either the symbol is not found, or something went
 ///   wrong with generating the start_function. False otherwise.
-bool rebuild_goto_start_functiont::operator()(
-  const irep_idt &entry_function)
+bool rebuild_goto_start_functiont::operator()()
 {
   const irep_idt &mode=get_entry_point_mode();
 
@@ -59,7 +58,7 @@ bool rebuild_goto_start_functiont::operator()(
   remove_existing_entry_point();
 
   bool return_code=
-    language->generate_start_function(entry_function, symbol_table);
+    language->generate_support_functions(symbol_table);
 
   // Remove the function from the goto_functions so it is copied back in
   // from the symbol table during goto_convert
diff --git a/src/goto-programs/rebuild_goto_start_function.h b/src/goto-programs/rebuild_goto_start_function.h
index 79086aac570..15516389fc4 100644
--- a/src/goto-programs/rebuild_goto_start_function.h
+++ b/src/goto-programs/rebuild_goto_start_function.h
@@ -30,7 +30,7 @@ class rebuild_goto_start_functiont: public messaget
     symbol_tablet &symbol_table,
     goto_functionst &goto_functions);
 
-  bool operator()(const irep_idt &entry_function);
+  bool operator()();
 
 private:
   irep_idt get_entry_point_mode() const;
diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp
index 4d4bb9e8cf8..afda2091079 100644
--- a/src/java_bytecode/java_bytecode_language.cpp
+++ b/src/java_bytecode/java_bytecode_language.cpp
@@ -109,30 +109,6 @@ void java_bytecode_languaget::modules_provided(std::set<std::string> &modules)
   // modules.insert(translation_unit(parse_path));
 }
 
-/// Generate a _start function for a specific function.
-/// \param entry_function_symbol_id: The symbol for the function that should be
-///   used as the entry point
-/// \param symbol_table: The symbol table for the program. The new _start
-///   function symbol will be added to this table
-/// \return Returns false if the _start method was generated correctly
-bool java_bytecode_languaget::generate_start_function(
-  const irep_idt &entry_function_symbol_id,
-  symbol_tablet &symbol_table)
-{
-  PRECONDITION(language_options_initialized);
-  const auto res=
-    get_main_symbol(
-      symbol_table, entry_function_symbol_id, get_message_handler());
-
-  return generate_java_start_function(
-    res.main_function,
-    symbol_table,
-    get_message_handler(),
-    assume_inputs_non_null,
-    object_factory_parameters,
-    *pointer_type_selector);
-}
-
 /// ANSI-C preprocessing
 bool java_bytecode_languaget::preprocess(
   std::istream &instream,
@@ -205,6 +181,8 @@ bool java_bytecode_languaget::typecheck(
 {
   PRECONDITION(language_options_initialized);
 
+  java_internal_additions(symbol_table);
+
   if(string_refinement_enabled)
     string_preprocess.initialize_conversion_table();
 
@@ -267,6 +245,27 @@ bool java_bytecode_languaget::typecheck(
   return false;
 }
 
+bool java_bytecode_languaget::generate_support_functions(
+  symbol_tablet &symbol_table)
+{
+  PRECONDITION(language_options_initialized);
+
+  main_function_resultt res=
+    get_main_symbol(symbol_table, main_class, get_message_handler());
+  if(res.stop_convert)
+    return res.error_found;
+
+  // generate the test harness in __CPROVER__start and a call the entry point
+  return
+    java_entry_point(
+      symbol_table,
+      main_class,
+      get_message_handler(),
+      assume_inputs_non_null,
+      object_factory_parameters,
+      get_pointer_type_selector());
+}
+
 /// Uses a simple context-insensitive ('ci') analysis to determine which methods
 /// may be reachable from the main entry point. In brief, static methods are
 /// reachable if we find a callsite in another reachable site, while virtual
@@ -391,25 +390,11 @@ void java_bytecode_languaget::replace_string_methods(
 bool java_bytecode_languaget::final(symbol_tablet &symbol_table)
 {
   PRECONDITION(language_options_initialized);
-  java_internal_additions(symbol_table);
 
   // replace code of String methods calls by code we generate
   replace_string_methods(symbol_table);
 
-  main_function_resultt res=
-    get_main_symbol(symbol_table, main_class, get_message_handler());
-  if(res.stop_convert)
-    return res.error_found;
-
-  // generate the test harness in __CPROVER__start and a call the entry point
-  return
-    java_entry_point(
-      symbol_table,
-      main_class,
-      get_message_handler(),
-      assume_inputs_non_null,
-      object_factory_parameters,
-      get_pointer_type_selector());
+  return false;
 }
 
 void java_bytecode_languaget::show_parse(std::ostream &out)
diff --git a/src/java_bytecode/java_bytecode_language.h b/src/java_bytecode/java_bytecode_language.h
index dd2a20eaafe..eac76e3aa06 100644
--- a/src/java_bytecode/java_bytecode_language.h
+++ b/src/java_bytecode/java_bytecode_language.h
@@ -98,6 +98,9 @@ class java_bytecode_languaget:public languaget
     std::istream &instream,
     const std::string &path) override;
 
+  bool generate_support_functions(
+    symbol_tablet &symbol_table) override;
+
   bool typecheck(
     symbol_tablet &context,
     const std::string &module) override;
@@ -154,10 +157,6 @@ class java_bytecode_languaget:public languaget
   virtual void convert_lazy_method(
     const irep_idt &id, symbol_tablet &) override;
 
-  virtual bool generate_start_function(
-    const irep_idt &entry_function_symbol_id,
-    class symbol_tablet &symbol_table) override;
-
 protected:
   bool do_ci_lazy_method_conversion(symbol_tablet &, lazy_methodst &);
   const select_pointer_typet &get_pointer_type_selector() const;
diff --git a/src/java_bytecode/java_entry_point.cpp b/src/java_bytecode/java_entry_point.cpp
index 17c7b5f96ed..08c1f44564b 100644
--- a/src/java_bytecode/java_entry_point.cpp
+++ b/src/java_bytecode/java_entry_point.cpp
@@ -13,6 +13,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <unordered_set>
 #include <iostream>
 
+#include <linking/static_lifetime_init.h>
+
 #include <util/arith_tools.h>
 #include <util/prefix.h>
 #include <util/std_types.h>
@@ -34,13 +36,15 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "java_types.h"
 #include "java_utils.h"
 
-#define INITIALIZE CPROVER_PREFIX "initialize"
-
 static void create_initialize(symbol_tablet &symbol_table)
 {
+  // If __CPROVER_initialize already exists, replace it. It may already exist
+  // if a GOTO binary provided it. This behaviour mirrors the ANSI-C frontend.
+  symbol_table.symbols.erase(INITIALIZE_FUNCTION);
+
   symbolt initialize;
-  initialize.name=INITIALIZE;
-  initialize.base_name=INITIALIZE;
+  initialize.name=INITIALIZE_FUNCTION;
+  initialize.base_name=INITIALIZE_FUNCTION;
   initialize.mode=ID_java;
 
   code_typet type;
@@ -59,8 +63,7 @@ static void create_initialize(symbol_tablet &symbol_table)
 
   initialize.value=init_code;
 
-  if(symbol_table.add(initialize))
-    throw "failed to add "+std::string(INITIALIZE);
+  symbol_table.add(initialize);
 }
 
 static bool should_init_symbol(const symbolt &sym)
@@ -93,7 +96,7 @@ void java_static_lifetime_init(
   const object_factory_parameterst &object_factory_parameters,
   const select_pointer_typet &pointer_type_selector)
 {
-  symbolt &initialize_symbol=symbol_table.lookup(INITIALIZE);
+  symbolt &initialize_symbol=symbol_table.lookup(INITIALIZE_FUNCTION);
   code_blockt &code_block=to_code_block(to_code(initialize_symbol.value));
 
   // We need to zero out all static variables, or nondet-initialize if they're
@@ -539,11 +542,11 @@ bool generate_java_start_function(
   // build call to initialization function
   {
     symbol_tablet::symbolst::iterator init_it=
-      symbol_table.symbols.find(INITIALIZE);
+      symbol_table.symbols.find(INITIALIZE_FUNCTION);
 
     if(init_it==symbol_table.symbols.end())
     {
-      message.error() << "failed to find " INITIALIZE " symbol"
+      message.error() << "failed to find " INITIALIZE_FUNCTION " symbol"
                       << messaget::eom;
       return true; // give up with error
     }
diff --git a/src/jsil/jsil_language.cpp b/src/jsil/jsil_language.cpp
index 94f16cc5cb8..83462732c1d 100644
--- a/src/jsil/jsil_language.cpp
+++ b/src/jsil/jsil_language.cpp
@@ -41,22 +41,6 @@ bool jsil_languaget::interfaces(symbol_tablet &symbol_table)
   return false;
 }
 
-/// Generate a _start function for a specific function
-/// \param entry_function_symbol_id: The symbol for the function that should be
-///   used as the entry point
-/// \param symbol_table: The symbol table for the program. The new _start
-///   function symbol will be added to this table
-/// \return Returns false if the _start method was generated correctly
-bool jsil_languaget::generate_start_function(
-  const irep_idt &entry_function_symbol_id,
-  symbol_tablet &symbol_table)
-{
-  // TODO(tkiley): This should be implemented if this language
-  // is used.
-  UNREACHABLE;
-  return true;
-}
-
 bool jsil_languaget::preprocess(
   std::istream &instream,
   const std::string &path,
@@ -102,14 +86,12 @@ bool jsil_languaget::typecheck(
   return false;
 }
 
-bool jsil_languaget::final(symbol_tablet &symbol_table)
+bool jsil_languaget::generate_support_functions(
+  symbol_tablet &symbol_table)
 {
-  if(jsil_entry_point(
-      symbol_table,
-      get_message_handler()))
-    return true;
-
-  return false;
+  return jsil_entry_point(
+    symbol_table,
+    get_message_handler());
 }
 
 void jsil_languaget::show_parse(std::ostream &out)
diff --git a/src/jsil/jsil_language.h b/src/jsil/jsil_language.h
index 6ff0c852bdb..91df43e6266 100644
--- a/src/jsil/jsil_language.h
+++ b/src/jsil/jsil_language.h
@@ -31,12 +31,13 @@ class jsil_languaget:public languaget
     std::istream &instream,
     const std::string &path) override;
 
+  virtual bool generate_support_functions(
+    symbol_tablet &symbol_table) override;
+
   virtual bool typecheck(
     symbol_tablet &context,
     const std::string &module) override;
 
-  virtual bool final(symbol_tablet &context) override;
-
   virtual void show_parse(std::ostream &out) override;
 
   virtual ~jsil_languaget();
@@ -69,10 +70,6 @@ class jsil_languaget:public languaget
   virtual void modules_provided(std::set<std::string> &modules) override;
   virtual bool interfaces(symbol_tablet &symbol_table) override;
 
-  virtual bool generate_start_function(
-    const irep_idt &entry_function_symbol_id,
-    class symbol_tablet &symbol_table) override;
-
 protected:
   jsil_parse_treet parse_tree;
   std::string parse_path;
diff --git a/src/util/language.h b/src/util/language.h
index d3b25165c3b..ee3cd40c827 100644
--- a/src/util/language.h
+++ b/src/util/language.h
@@ -28,6 +28,12 @@ class namespacet;
 class typet;
 class cmdlinet;
 
+#define OPT_FUNCTIONS \
+  "(function):"
+
+#define HELP_FUNCTIONS \
+  " --function name              set main function name\n"
+
 class languaget:public messaget
 {
 public:
@@ -45,6 +51,17 @@ class languaget:public messaget
     std::istream &instream,
     const std::string &path)=0;
 
+  /// Create language-specific support functions, such as __CPROVER_start,
+  /// __CPROVER_initialize and language-specific library functions.
+  /// This runs after the `typecheck` phase but before lazy function loading.
+  /// Anything that must wait until lazy function loading is done can be
+  /// deferred until `final`, which runs after lazy function loading is
+  /// complete. Functions introduced here are visible to lazy loading and
+  /// can influence its decisions (e.g. picking the types of input parameters
+  /// and globals), whereas anything introduced during `final` cannot.
+  virtual bool generate_support_functions(
+    symbol_tablet &symbol_table)=0;
+
   // add external dependencies of a given module to set
 
   virtual void dependencies(
@@ -65,8 +82,8 @@ class languaget:public messaget
   virtual void convert_lazy_method(const irep_idt &id, symbol_tablet &)
   { }
 
-  // final adjustments, e.g., initialization and call to main()
-
+  /// Final adjustments, e.g. initializing stub functions and globals that
+  /// were discovered during function loading
   virtual bool final(
     symbol_tablet &symbol_table);
 
@@ -119,10 +136,6 @@ class languaget:public messaget
 
   void set_should_generate_opaque_method_stubs(bool should_generate_stubs);
 
-  virtual bool generate_start_function(
-    const irep_idt &entry_function_symbol_id,
-    class symbol_tablet &symbol_table)=0;
-
   // constructor / destructor
 
   languaget() { }
diff --git a/src/util/language_file.cpp b/src/util/language_file.cpp
index 300dccd93be..a90fb6f3e9e 100644
--- a/src/util/language_file.cpp
+++ b/src/util/language_file.cpp
@@ -41,9 +41,8 @@ void language_filet::convert_lazy_method(
 
 void language_filest::show_parse(std::ostream &out)
 {
-  for(file_mapt::iterator it=file_map.begin();
-      it!=file_map.end(); it++)
-    it->second.language->show_parse(out);
+  for(const auto &file : file_map)
+    file.second.language->show_parse(out);
 }
 
 /// Turn on or off stub generation for all the languages
@@ -60,32 +59,31 @@ void language_filest::set_should_generate_opaque_method_stubs(
 
 bool language_filest::parse()
 {
-  for(file_mapt::iterator it=file_map.begin();
-      it!=file_map.end(); it++)
+  for(auto &file : file_map)
   {
     // open file
 
-    std::ifstream infile(it->first);
+    std::ifstream infile(file.first);
 
     if(!infile)
     {
-      error() << "Failed to open " << it->first << eom;
+      error() << "Failed to open " << file.first << eom;
       return true;
     }
 
     // parse it
 
-    languaget &language=*(it->second.language);
+    languaget &language=*(file.second.language);
 
-    if(language.parse(infile, it->first))
+    if(language.parse(infile, file.first))
     {
-      error() << "Parsing of " << it->first << " failed" << eom;
+      error() << "Parsing of " << file.first << " failed" << eom;
       return true;
     }
 
     // what is provided?
 
-    it->second.get_modules();
+    file.second.get_modules();
   }
 
   return false;
@@ -95,10 +93,9 @@ bool language_filest::typecheck(symbol_tablet &symbol_table)
 {
   // typecheck interfaces
 
-  for(file_mapt::iterator it=file_map.begin();
-      it!=file_map.end(); it++)
+  for(auto &file : file_map)
   {
-    if(it->second.language->interfaces(symbol_table))
+    if(file.second.language->interfaces(symbol_table))
       return true;
   }
 
@@ -106,11 +103,10 @@ bool language_filest::typecheck(symbol_tablet &symbol_table)
 
   unsigned collision_counter=0;
 
-  for(file_mapt::iterator fm_it=file_map.begin();
-      fm_it!=file_map.end(); fm_it++)
+  for(auto &file : file_map)
   {
     const language_filet::modulest &modules=
-      fm_it->second.modules;
+      file.second.modules;
 
     for(language_filet::modulest::const_iterator
         mo_it=modules.begin();
@@ -127,7 +123,7 @@ bool language_filest::typecheck(symbol_tablet &symbol_table)
       }
 
       language_modulet module;
-      module.file=&fm_it->second;
+      module.file=&file.second;
       module.name=module_name;
       module_map.insert(
         std::pair<std::string, language_modulet>(module.name, module));
@@ -136,45 +132,57 @@ bool language_filest::typecheck(symbol_tablet &symbol_table)
 
   // typecheck files
 
-  for(file_mapt::iterator it=file_map.begin();
-      it!=file_map.end(); it++)
+  for(auto &file : file_map)
   {
-    if(it->second.modules.empty())
+    if(file.second.modules.empty())
     {
-      if(it->second.language->typecheck(symbol_table, ""))
+      if(file.second.language->typecheck(symbol_table, ""))
         return true;
       // register lazy methods.
       // TODO: learn about modules and generalise this
       // to module-providing languages if required.
       std::set<irep_idt> lazy_method_ids;
-      it->second.language->lazy_methods_provided(lazy_method_ids);
+      file.second.language->lazy_methods_provided(lazy_method_ids);
       for(const auto &id : lazy_method_ids)
-        lazy_method_map[id]=&it->second;
+        lazy_method_map[id]=&file.second;
     }
   }
 
   // typecheck modules
 
-  for(module_mapt::iterator it=module_map.begin();
-      it!=module_map.end(); it++)
+  for(auto &module : module_map)
   {
-    if(typecheck_module(symbol_table, it->second))
+    if(typecheck_module(symbol_table, module.second))
       return true;
   }
 
   return false;
 }
 
+bool language_filest::generate_support_functions(
+  symbol_tablet &symbol_table)
+{
+  std::set<std::string> languages;
+
+  for(auto &file : file_map)
+  {
+    if(languages.insert(file.second.language->id()).second)
+      if(file.second.language->generate_support_functions(symbol_table))
+        return true;
+  }
+
+  return false;
+}
+
 bool language_filest::final(
   symbol_tablet &symbol_table)
 {
   std::set<std::string> languages;
 
-  for(file_mapt::iterator it=file_map.begin();
-      it!=file_map.end(); it++)
+  for(auto &file : file_map)
   {
-    if(languages.insert(it->second.language->id()).second)
-      if(it->second.language->final(symbol_table))
+    if(languages.insert(file.second.language->id()).second)
+      if(file.second.language->final(symbol_table))
         return true;
   }
 
@@ -184,10 +192,9 @@ bool language_filest::final(
 bool language_filest::interfaces(
   symbol_tablet &symbol_table)
 {
-  for(file_mapt::iterator it=file_map.begin();
-      it!=file_map.end(); it++)
+  for(auto &file : file_map)
   {
-    if(it->second.language->interfaces(symbol_table))
+    if(file.second.language->interfaces(symbol_table))
       return true;
   }
 
diff --git a/src/util/language_file.h b/src/util/language_file.h
index e414182e3c5..c00e4155252 100644
--- a/src/util/language_file.h
+++ b/src/util/language_file.h
@@ -83,6 +83,8 @@ class language_filest:public messaget
 
   void show_parse(std::ostream &out);
 
+  bool generate_support_functions(symbol_tablet &symbol_table);
+
   bool typecheck(symbol_tablet &symbol_table);
 
   bool final(symbol_tablet &symbol_table);