Merge pull request #1394 from smowton/smowton/feature/split_frontend_final_stage

Split the entry-point-generation phase into two parts

Author: smowton

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;