Call generate_start_function only when regenerating the start function

Rather than calling the final method, call a refactored out method that
is just responsible for generating the _start body.

Author: thk123

src/ansi-c/ansi_c_entry_point.cpp

@@ -18,6 +18,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/config.h>
 #include <util/cprover_prefix.h>
 #include <util/prefix.h>
+#include <util/symbol.h>
 
 #include <util/c_types.h>
 #include <ansi-c/string_constant.h>
@@ -190,6 +191,22 @@ bool ansi_c_entry_point(
   if(static_lifetime_init(symbol_table, symbol.location, message_handler))
     return true;
 
+  return generate_ansi_c_start_function(symbol, symbol_table, message_handler);
+}
+
+
+/// Generate a _start function for a specific function
+/// \param entry_function_symbol: 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 generate_ansi_c_start_function(
+  const symbolt &symbol,
+  symbol_tablet &symbol_table,
+  message_handlert &message_handler)
+{
+  PRECONDITION(!symbol.value.is_nil());
   code_blockt init_code;
 
   // build call to initialization function
@@ -237,7 +254,7 @@ bool ansi_c_entry_point(
   const code_typet::parameterst &parameters=
     to_code_type(symbol.type).parameters();
 
-  if(symbol.name==standard_main)
+  if(symbol.name==ID_main)
   {
     if(parameters.empty())
     {

src/ansi-c/ansi_c_entry_point.h

@@ -18,4 +18,9 @@ bool ansi_c_entry_point(
   const std::string &standard_main,
   message_handlert &message_handler);
 
+bool generate_ansi_c_start_function(
+  const symbolt &symbol,
+  symbol_tablet &symbol_table,
+  message_handlert &message_handler);
+
 #endif // CPROVER_ANSI_C_ANSI_C_ENTRY_POINT_H

src/ansi-c/ansi_c_language.cpp

@@ -36,6 +36,22 @@ 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: 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 symbolt &entry_function_symbol,
+  symbol_tablet &symbol_table)
+{
+  return generate_ansi_c_start_function(
+    entry_function_symbol,
+    symbol_table,
+    *message_handler);
+}
+
 /// ANSI-C preprocessing
 bool ansi_c_languaget::preprocess(
   std::istream &instream,

src/ansi-c/ansi_c_language.h

@@ -73,6 +73,10 @@ class ansi_c_languaget:public languaget
 
   void modules_provided(std::set<std::string> &modules) override;
 
+  virtual bool generate_start_function(
+    const class symbolt &entry_function_symbol,
+    class symbol_tablet &symbol_table) override;
+
 protected:
   ansi_c_parse_treet parse_tree;
   std::string parse_path;

src/util/language.cpp

@@ -194,6 +194,22 @@ void languaget::generate_opaque_parameter_symbols(
   }
 }
 
+/// Generate a entry function for a specific function. Should be overriden in
+/// derived languagets
+/// \param entry_function_symbol: 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 entry method was generated correctly
+bool languaget::generate_start_function(
+  const symbolt &entry_function_symbol,
+  symbol_tablet &symbol_table)
+{
+  // Implement in derived languagets
+  assert(0);
+  return true;
+}
+
 /// To replace an existing _start function with a new one that calls a specified
 /// function
 /// \param required_entry_function: a code symbol inside the symbol table which
@@ -205,18 +221,14 @@ void languaget::generate_opaque_parameter_symbols(
 /// \return Returns false if the new start function is created successfully,
 ///   true otherwise.
 bool languaget::regenerate_start_function(
-  const symbolt &required_entry_function,
+  const symbolt &entry_function_symbol,
   symbol_tablet &symbol_table,
   goto_functionst &goto_functions)
 {
   // Remove the existing _start function so we can create a new one
   symbol_table.remove(goto_functionst::entry_point());
-  config.main=required_entry_function.name.c_str();
 
-  // TODO(tkiley): calling final is not really correct (in fact for example,
-  // opaque function stubs get generated here). Instead the final method should
-  // call this to generate the function in the first place.
-  bool return_code=final(symbol_table);
+  bool return_code=generate_start_function(entry_function_symbol, symbol_table);
 
   // Remove the function from the goto_functions so is copied back in
   // from the symbol table

src/util/language.h

@@ -119,8 +119,12 @@ class languaget:public messaget
 
   void set_should_generate_opaque_method_stubs(bool should_generate_stubs);
 
+  virtual bool generate_start_function(
+    const class symbolt &entry_function_symbol,
+    class symbol_tablet &symbol_table);
+
   bool regenerate_start_function(
-    const class symbolt &required_entry_function,
+    const class symbolt &entry_function_symbol,
     symbol_tablet &symbol_table,
     class goto_functionst &goto_functions);