Merge pull request #1483 from diffblue/signature_initialize_goto_model

initialize_goto_model now returns a goto_model

Author: Daniel Kroening

src/cbmc/cbmc_parse_options.cpp

@@ -611,10 +611,7 @@ int cbmc_parse_optionst::get_goto_program(
 
   try
   {
-    if(initialize_goto_model(goto_model, cmdline, get_message_handler()))
-    // Remove all binaries from the command line as they
-    // are already compiled
-      return 6;
+    goto_model=initialize_goto_model(cmdline, get_message_handler());
 
     if(cmdline.isset("show-symbol-table"))
     {

src/clobber/clobber_parse_options.cpp

@@ -124,8 +124,7 @@ int clobber_parse_optionst::doit()
 
   try
   {
-    if(initialize_goto_model(goto_model, cmdline, get_message_handler()))
-      return 6;
+    goto_model=initialize_goto_model(cmdline, get_message_handler());
 
     label_properties(goto_model);
 

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -160,8 +160,27 @@ int goto_analyzer_parse_optionst::doit()
 
   register_languages();
 
-  if(initialize_goto_model(goto_model, cmdline, get_message_handler()))
-    return 6;
+  try
+  {
+    goto_model=initialize_goto_model(cmdline, get_message_handler());
+  }
+
+  catch(const char *e)
+  {
+    error() << e << eom;
+    return true;
+  }
+
+  catch(const std::string e)
+  {
+    error() << e << eom;
+    return true;
+  }
+
+  catch(int)
+  {
+    return true;
+  }
 
   if(process_goto_program(options))
     return 6;

src/goto-programs/initialize_goto_model.cpp

@@ -26,8 +26,7 @@ Author: Daniel Kroening, [email protected]
 #include "goto_convert_functions.h"
 #include "read_goto_binary.h"
 
-bool initialize_goto_model(
-  goto_modelt &goto_model,
+goto_modelt initialize_goto_model(
   const cmdlinet &cmdline,
   message_handlert &message_handler)
 {
@@ -36,168 +35,148 @@ bool initialize_goto_model(
   if(files.empty())
   {
     msg.error() << "Please provide a program" << messaget::eom;
-    return true;
+    throw 0;
   }
 
-  try
+  std::vector<std::string> binaries, sources;
+  binaries.reserve(files.size());
+  sources.reserve(files.size());
+
+  for(const auto &file : files)
   {
-    std::vector<std::string> binaries, sources;
-    binaries.reserve(files.size());
-    sources.reserve(files.size());
+    if(is_goto_binary(file))
+      binaries.push_back(file);
+    else
+      sources.push_back(file);
+  }
 
-    for(const auto &file : files)
-    {
-      if(is_goto_binary(file))
-        binaries.push_back(file);
-      else
-        sources.push_back(file);
-    }
+  language_filest language_files;
+  language_files.set_message_handler(message_handler);
 
-    language_filest language_files;
-    language_files.set_message_handler(message_handler);
+  goto_modelt goto_model;
 
-    if(!sources.empty())
+  if(!sources.empty())
+  {
+    for(const auto &filename : sources)
     {
-      for(const auto &filename : sources)
+      #ifdef _MSC_VER
+      std::ifstream infile(widen(filename));
+      #else
+      std::ifstream infile(filename);
+      #endif
+
+      if(!infile)
       {
-        #ifdef _MSC_VER
-        std::ifstream infile(widen(filename));
-        #else
-        std::ifstream infile(filename);
-        #endif
-
-        if(!infile)
-        {
-          msg.error() << "failed to open input file `" << filename
-            << '\'' << messaget::eom;
-          return true;
-        }
-
-        std::pair<language_filest::file_mapt::iterator, bool>
-          result=language_files.file_map.insert(
-            std::pair<std::string, language_filet>(filename, language_filet()));
-
-        language_filet &lf=result.first->second;
-
-        lf.filename=filename;
-        lf.language=get_language_from_filename(filename);
-
-        if(lf.language==nullptr)
-        {
-          source_locationt location;
-          location.set_file(filename);
-          msg.error().source_location=location;
-          msg.error() << "failed to figure out type of file" << messaget::eom;
-          return true;
-        }
-
-        languaget &language=*lf.language;
-        language.set_message_handler(message_handler);
-        language.get_language_options(cmdline);
-
-        msg.status() << "Parsing " << filename << messaget::eom;
-
-        if(language.parse(infile, filename))
-        {
-          msg.error() << "PARSING ERROR" << messaget::eom;
-          return true;
-        }
-
-        lf.get_modules();
+        msg.error() << "failed to open input file `" << filename
+          << '\'' << messaget::eom;
+        throw 0;
       }
 
-      msg.status() << "Converting" << messaget::eom;
+      std::pair<language_filest::file_mapt::iterator, bool>
+        result=language_files.file_map.insert(
+          std::pair<std::string, language_filet>(filename, language_filet()));
 
-      if(language_files.typecheck(goto_model.symbol_table))
-      {
-        msg.error() << "CONVERSION ERROR" << messaget::eom;
-        return true;
-      }
-    }
+      language_filet &lf=result.first->second;
 
-    for(const auto &file : binaries)
-    {
-      msg.status() << "Reading GOTO program from file" << messaget::eom;
+      lf.filename=filename;
+      lf.language=get_language_from_filename(filename);
 
-      if(read_object_and_link(file, goto_model, message_handler))
-        return true;
-    }
+      if(lf.language==nullptr)
+      {
+        source_locationt location;
+        location.set_file(filename);
+        msg.error().source_location=location;
+        msg.error() << "failed to figure out type of file" << messaget::eom;
+        throw 0;
+      }
 
-    bool binaries_provided_start=
-      goto_model.symbol_table.has_symbol(goto_functionst::entry_point());
+      languaget &language=*lf.language;
+      language.set_message_handler(message_handler);
+      language.get_language_options(cmdline);
 
-    bool entry_point_generation_failed=false;
+      msg.status() << "Parsing " << filename << messaget::eom;
 
-    if(binaries_provided_start && cmdline.isset("function"))
-    {
-      // 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())
+      if(language.parse(infile, filename))
       {
-        // 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);
+        msg.error() << "PARSING ERROR" << messaget::eom;
+        throw 0;
       }
 
-      // 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);
+      lf.get_modules();
     }
 
-    if(entry_point_generation_failed)
-    {
-      msg.error() << "SUPPORT FUNCTION GENERATION ERROR" << messaget::eom;
-      return true;
-    }
+    msg.status() << "Converting" << messaget::eom;
 
-    if(language_files.final(goto_model.symbol_table))
+    if(language_files.typecheck(goto_model.symbol_table))
     {
-      msg.error() << "FINAL STAGE CONVERSION ERROR" << messaget::eom;
-      return true;
+      msg.error() << "CONVERSION ERROR" << messaget::eom;
+      throw 0;
     }
+  }
 
-    msg.status() << "Generating GOTO Program" << messaget::eom;
-
-    goto_convert(
-      goto_model.symbol_table,
-      goto_model.goto_functions,
-      message_handler);
+  for(const auto &file : binaries)
+  {
+    msg.status() << "Reading GOTO program from file" << messaget::eom;
 
-    // stupid hack
-    config.set_object_bits_from_symbol_table(
-      goto_model.symbol_table);
+    if(read_object_and_link(file, goto_model, message_handler))
+      throw 0;
   }
-  catch(const char *e)
+
+  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"))
   {
-    msg.error() << e << messaget::eom;
-    return true;
+    // 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();
   }
-  catch(const std::string e)
+  else if(!binaries_provided_start)
   {
-    msg.error() << e << messaget::eom;
-    return true;
+    // 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);
+    }
+
+    // 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);
   }
-  catch(int)
+
+  if(entry_point_generation_failed)
   {
-    return true;
+    msg.error() << "SUPPORT FUNCTION GENERATION ERROR" << messaget::eom;
+    throw 0;
   }
-  catch(std::bad_alloc)
+
+  if(language_files.final(goto_model.symbol_table))
   {
-    msg.error() << "Out of memory" << messaget::eom;
-    return true;
+    msg.error() << "FINAL STAGE CONVERSION ERROR" << messaget::eom;
+    throw 0;
   }
 
-  return false; // no error
+  msg.status() << "Generating GOTO Program" << messaget::eom;
+
+  goto_convert(
+    goto_model.symbol_table,
+    goto_model.goto_functions,
+    message_handler);
+
+  // stupid hack
+  config.set_object_bits_from_symbol_table(
+    goto_model.symbol_table);
+
+  return goto_model;
 }

src/goto-programs/initialize_goto_model.h

@@ -17,8 +17,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "goto_model.h"
 
-bool initialize_goto_model(
-  goto_modelt &goto_model,
+goto_modelt initialize_goto_model(
   const cmdlinet &cmdline,
   message_handlert &message_handler);