SSS: Make _start optional

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;
 }

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;
 

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;
 }

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;
 

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;

src/goto-programs/get_goto_model.h

@@ -16,7 +16,9 @@ Author: Daniel Kroening, [email protected]
 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

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());

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;
 

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;
 }

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);
 

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;

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

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;
 }

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
 

src/util/language_file.cpp

@@ -235,15 +235,16 @@ 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;
 
   for(file_mapt::iterator it=file_map.begin();
       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;
   }
 

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);