Split the entry-point-generation phase into two parts

regression/goto-cc-cbmc/mixed-c-library-goto-main/lib.c

@@ -0,0 +1,4 @@
+
+int getone() {
+  return 1;
+}

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

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

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

regression/goto-cc-cbmc/mixed-goto-library-c-main/lib.c

@@ -0,0 +1,4 @@
+
+int getone() {
+  return 1;
+}

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

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

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

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)

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;

src/cbmc/cbmc_parse_options.cpp

@@ -52,7 +52,6 @@ Author: Daniel Kroening, [email protected]
 #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());

src/cbmc/cbmc_parse_options.h

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

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)

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;

src/goto-analyzer/goto_analyzer_parse_options.h

@@ -14,10 +14,10 @@ Author: Daniel Kroening, [email protected]
 
 #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>
 

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;

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

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;