diff --git a/src/ansi-c/ansi_c_language.cpp b/src/ansi-c/ansi_c_language.cpp
index dc69515ede2..8eff2a1d82c 100644
--- a/src/ansi-c/ansi_c_language.cpp
+++ b/src/ansi-c/ansi_c_language.cpp
@@ -194,10 +194,15 @@ Function: ansi_c_languaget::final
 
 \*******************************************************************/
 
-bool ansi_c_languaget::final(symbol_tablet &symbol_table)
+bool ansi_c_languaget::final(
+  symbol_tablet &symbol_table,
+  bool generate_start_function)
 {
-  if(ansi_c_entry_point(symbol_table, "main", get_message_handler()))
-    return true;
+  if(generate_start_function)
+  {
+    if(ansi_c_entry_point(symbol_table, "main", get_message_handler()))
+      return true;
+  }
 
   return false;
 }
diff --git a/src/ansi-c/ansi_c_language.h b/src/ansi-c/ansi_c_language.h
index 9f6fba0cc9b..0dd1d8bb6fa 100644
--- a/src/ansi-c/ansi_c_language.h
+++ b/src/ansi-c/ansi_c_language.h
@@ -35,7 +35,8 @@ class ansi_c_languaget:public languaget
     const std::string &module) override;
 
   bool final(
-    symbol_tablet &symbol_table) override;
+    symbol_tablet &symbol_table,
+    bool generate_start_function) override;
 
   void show_parse(std::ostream &out) override;
 
diff --git a/src/cpp/cpp_language.cpp b/src/cpp/cpp_language.cpp
index f1b4b97018d..11ff42414f1 100644
--- a/src/cpp/cpp_language.cpp
+++ b/src/cpp/cpp_language.cpp
@@ -201,10 +201,15 @@ Function: cpp_languaget::final
 
 \*******************************************************************/
 
-bool cpp_languaget::final(symbol_tablet &symbol_table)
+bool cpp_languaget::final(
+  symbol_tablet &symbol_table,
+  bool generate_start_function)
 {
-  if(ansi_c_entry_point(symbol_table, "main", get_message_handler()))
-    return true;
+  if(generate_start_function)
+  {
+    if(ansi_c_entry_point(symbol_table, "main", get_message_handler()))
+      return true;
+  }
 
   return false;
 }
diff --git a/src/cpp/cpp_language.h b/src/cpp/cpp_language.h
index 329adbaa1a5..32a4e281f78 100644
--- a/src/cpp/cpp_language.h
+++ b/src/cpp/cpp_language.h
@@ -41,7 +41,8 @@ class cpp_languaget:public languaget
     class replace_symbolt &replace_symbol) const;
 
   bool final(
-    symbol_tablet &symbol_table) override;
+    symbol_tablet &symbol_table,
+    bool generate_start_function) override;
 
   void show_parse(std::ostream &out) override;
 
diff --git a/src/goto-programs/get_goto_model.cpp b/src/goto-programs/get_goto_model.cpp
index 02aae876030..810e4b72ec7 100644
--- a/src/goto-programs/get_goto_model.cpp
+++ b/src/goto-programs/get_goto_model.cpp
@@ -114,7 +114,7 @@ bool get_goto_modelt::operator()(const std::vector<std::string> &files)
 
       if(binaries.empty())
       {
-        if(language_files.final(symbol_table))
+        if(language_files.final(symbol_table, generate_start_function))
         {
           error() << "CONVERSION ERROR" << eom;
           return true;
diff --git a/src/goto-programs/get_goto_model.h b/src/goto-programs/get_goto_model.h
index 84c6c00c7a5..3027f1a2af2 100644
--- a/src/goto-programs/get_goto_model.h
+++ b/src/goto-programs/get_goto_model.h
@@ -16,7 +16,9 @@ Author: Daniel Kroening, kroening@kroening.com
 class get_goto_modelt:public goto_modelt, public messaget
 {
 public:
+  get_goto_modelt() : generate_start_function(true) {}
   bool operator()(const std::vector<std::string> &);
+  bool generate_start_function;
 };
 
 #endif // CPROVER_GOTO_PROGRAMS_GET_GOTO_MODEL_H
diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp
index 668960dbe17..0864c82b160 100644
--- a/src/java_bytecode/java_bytecode_language.cpp
+++ b/src/java_bytecode/java_bytecode_language.cpp
@@ -744,13 +744,17 @@ Function: java_bytecode_languaget::final
 
 \*******************************************************************/
 
-bool java_bytecode_languaget::final(symbol_tablet &symbol_table)
+bool java_bytecode_languaget::final(
+  symbol_tablet &symbol_table,
+  bool generate_start_function)
 {
   /*
   if(c_final(symbol_table, message_handler)) return true;
   */
   java_internal_additions(symbol_table);
 
+  if(!generate_start_function)
+    return false;
 
   main_function_resultt res=
     get_main_symbol(symbol_table, main_class, get_message_handler());
diff --git a/src/java_bytecode/java_bytecode_language.h b/src/java_bytecode/java_bytecode_language.h
index 643eacd5b7f..46a308ca5fd 100644
--- a/src/java_bytecode/java_bytecode_language.h
+++ b/src/java_bytecode/java_bytecode_language.h
@@ -49,7 +49,8 @@ class java_bytecode_languaget:public languaget
     const std::string &module) override;
 
   bool final(
-    symbol_tablet &context) override;
+    symbol_tablet &context,
+    bool generate_start_function) override;
 
   void show_parse(std::ostream &out) override;
 
diff --git a/src/jsil/jsil_language.cpp b/src/jsil/jsil_language.cpp
index 6c022e65069..e7277e90728 100644
--- a/src/jsil/jsil_language.cpp
+++ b/src/jsil/jsil_language.cpp
@@ -165,12 +165,17 @@ Function: jsil_languaget::final
 
 \*******************************************************************/
 
-bool jsil_languaget::final(symbol_tablet &symbol_table)
+bool jsil_languaget::final(
+  symbol_tablet &symbol_table,
+  bool generate_start_function)
 {
-  if(jsil_entry_point(
-      symbol_table,
-      get_message_handler()))
-    return true;
+  if(generate_start_function)
+  {
+    if(jsil_entry_point(
+         symbol_table,
+         get_message_handler()))
+      return true;
+  }
 
   return false;
 }
diff --git a/src/jsil/jsil_language.h b/src/jsil/jsil_language.h
index 349f0b58740..39fe8f27808 100644
--- a/src/jsil/jsil_language.h
+++ b/src/jsil/jsil_language.h
@@ -30,7 +30,8 @@ class jsil_languaget:public languaget
     const std::string &module);
 
   virtual bool final(
-    symbol_tablet &context);
+    symbol_tablet &context,
+    bool generate_start_function);
 
   virtual void show_parse(std::ostream &out);
 
diff --git a/src/langapi/language_ui.cpp b/src/langapi/language_ui.cpp
index 95b5d104a4f..55badd462f1 100644
--- a/src/langapi/language_ui.cpp
+++ b/src/langapi/language_ui.cpp
@@ -34,7 +34,8 @@ language_uit::language_uit(
   const cmdlinet &__cmdline,
   ui_message_handlert &_ui_message_handler):
   ui_message_handler(_ui_message_handler),
-  _cmdline(__cmdline)
+  _cmdline(__cmdline),
+  generate_start_function(true)
 {
   set_message_handler(ui_message_handler);
 }
@@ -183,7 +184,7 @@ bool language_uit::final()
 {
   language_files.set_message_handler(*message_handler);
 
-  if(language_files.final(symbol_table))
+  if(language_files.final(symbol_table, generate_start_function))
   {
     if(get_ui()==ui_message_handlert::PLAIN)
       std::cerr << "CONVERSION ERROR" << std::endl;
diff --git a/src/langapi/language_ui.h b/src/langapi/language_ui.h
index 90c1de3e5cb..4258a03e6a3 100644
--- a/src/langapi/language_ui.h
+++ b/src/langapi/language_ui.h
@@ -52,6 +52,7 @@ class language_uit:public messaget
 
 protected:
   const cmdlinet &_cmdline;
+  bool generate_start_function;
 };
 
 #endif // CPROVER_LANGAPI_LANGUAGE_UI_H
diff --git a/src/util/language.cpp b/src/util/language.cpp
index 4b4a1ba4ae4..937df8b8a92 100644
--- a/src/util/language.cpp
+++ b/src/util/language.cpp
@@ -21,7 +21,7 @@ Function: languaget::final
 
 \*******************************************************************/
 
-bool languaget::final(symbol_tablet &symbol_table)
+bool languaget::final(symbol_tablet &symbol_table, bool generate_start_function)
 {
   return false;
 }
diff --git a/src/util/language.h b/src/util/language.h
index b19615496ec..6a97ec0a917 100644
--- a/src/util/language.h
+++ b/src/util/language.h
@@ -61,7 +61,8 @@ class languaget:public messaget
   // final adjustments, e.g., initialization and call to main()
 
   virtual bool final(
-    symbol_tablet &symbol_table);
+    symbol_tablet &symbol_table,
+    bool generate_start_function);
 
   // type check interfaces of currently parsed file
 
diff --git a/src/util/language_file.cpp b/src/util/language_file.cpp
index 46f51564b54..b8f0b779502 100644
--- a/src/util/language_file.cpp
+++ b/src/util/language_file.cpp
@@ -235,7 +235,8 @@ Function: language_filest::final
 \*******************************************************************/
 
 bool language_filest::final(
-  symbol_tablet &symbol_table)
+  symbol_tablet &symbol_table,
+  bool generate_start_function)
 {
   std::set<std::string> languages;
 
@@ -243,7 +244,7 @@ bool language_filest::final(
       it!=file_map.end(); it++)
   {
     if(languages.insert(it->second.language->id()).second)
-      if(it->second.language->final(symbol_table))
+      if(it->second.language->final(symbol_table, generate_start_function))
         return true;
   }
 
diff --git a/src/util/language_file.h b/src/util/language_file.h
index d3184d48697..959a5dcafc8 100644
--- a/src/util/language_file.h
+++ b/src/util/language_file.h
@@ -81,7 +81,7 @@ class language_filest:public messaget
 
   bool typecheck(symbol_tablet &symbol_table);
 
-  bool final(symbol_tablet &symbol_table);
+  bool final(symbol_tablet &symbol_table, bool generate_start_function);
 
   bool interfaces(symbol_tablet &symbol_table);