Replaced get_goto_modelt with initialize_goto_model

This initialisation does not need to be done by a derived class - it does not use any private members - and doing so prevents creating other derived classes

Author: NathanJPhillips

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -214,9 +214,7 @@ int goto_analyzer_parse_optionst::doit()
 
   register_languages();
 
-  goto_model.set_message_handler(get_message_handler());
-
-  if(goto_model(cmdline))
+  if(initialize_goto_model(goto_model, cmdline, get_message_handler()))
     return 6;
 
   if(process_goto_program(options))

src/goto-analyzer/goto_analyzer_parse_options.h

@@ -56,7 +56,7 @@ class goto_analyzer_parse_optionst:
 
 protected:
   ui_message_handlert ui_message_handler;
-  get_goto_modelt goto_model;
+  goto_modelt goto_model;
 
   virtual void register_languages();
 

src/goto-programs/get_goto_model.cpp

@@ -22,7 +22,7 @@ Author: Daniel Kroening, [email protected]
 
 /*******************************************************************\
 
-Function: get_goto_modelt::operator()
+Function: initialize_goto_model
 
   Inputs:
 
@@ -32,12 +32,16 @@ Function: get_goto_modelt::operator()
 
 \*******************************************************************/
 
-bool get_goto_modelt::operator()(const cmdlinet &_cmdline)
+bool initialize_goto_model(
+  goto_modelt &goto_model,
+  const cmdlinet &cmdline,
+  message_handlert &message_handler)
 {
-  const std::vector<std::string> &files=_cmdline.args;
+  messaget msg(message_handler);
+  const std::vector<std::string> &files=cmdline.args;
   if(files.empty())
   {
-    error() << "Please provide a program" << eom;
+    msg.error() << "Please provide a program" << messaget::eom;
     return true;
   }
 
@@ -59,7 +63,7 @@ bool get_goto_modelt::operator()(const cmdlinet &_cmdline)
     {
       language_filest language_files;
 
-      language_files.set_message_handler(get_message_handler());
+      language_files.set_message_handler(message_handler);
 
       for(const auto &filename : sources)
       {
@@ -71,8 +75,8 @@ bool get_goto_modelt::operator()(const cmdlinet &_cmdline)
 
         if(!infile)
         {
-          error() << "failed to open input file `" << filename
-                  << '\'' << eom;
+          msg.error() << "failed to open input file `" << filename
+            << '\'' << messaget::eom;
           return true;
         }
 
@@ -87,81 +91,78 @@ bool get_goto_modelt::operator()(const cmdlinet &_cmdline)
 
         if(lf.language==NULL)
         {
-          error("failed to figure out type of file", filename);
+          msg.error("failed to figure out type of file", filename);
           return true;
         }
 
         languaget &language=*lf.language;
-        language.set_message_handler(get_message_handler());
-        language.get_language_options(_cmdline);
+        language.set_message_handler(message_handler);
+        language.get_language_options(cmdline);
 
-        status() << "Parsing " << filename << eom;
+        msg.status() << "Parsing " << filename << messaget::eom;
 
         if(language.parse(infile, filename))
         {
-          error() << "PARSING ERROR" << eom;
+          msg.error() << "PARSING ERROR" << messaget::eom;
           return true;
         }
 
         lf.get_modules();
       }
 
-      status() << "Converting" << eom;
+      msg.status() << "Converting" << messaget::eom;
 
-      if(language_files.typecheck(symbol_table))
+      if(language_files.typecheck(goto_model.symbol_table))
       {
-        error() << "CONVERSION ERROR" << eom;
+        msg.error() << "CONVERSION ERROR" << messaget::eom;
         return true;
       }
 
       if(binaries.empty())
       {
-        if(language_files.final(symbol_table))
+        if(language_files.final(goto_model.symbol_table))
         {
-          error() << "CONVERSION ERROR" << eom;
+          msg.error() << "CONVERSION ERROR" << messaget::eom;
           return true;
         }
       }
     }
 
     for(const auto &file : binaries)
     {
-      status() << "Reading GOTO program from file" << eom;
+      msg.status() << "Reading GOTO program from file" << messaget::eom;
 
-      if(read_object_and_link(file, *this, get_message_handler()))
+      if(read_object_and_link(file, goto_model, message_handler))
         return true;
     }
 
     if(!binaries.empty())
-      config.set_from_symbol_table(symbol_table);
+      config.set_from_symbol_table(goto_model.symbol_table);
 
-    status() << "Generating GOTO Program" << eom;
+    msg.status() << "Generating GOTO Program" << messaget::eom;
 
-    goto_convert(symbol_table,
-                 goto_functions,
-                 get_message_handler());
+    goto_convert(
+      goto_model.symbol_table,
+      goto_model.goto_functions,
+      message_handler);
   }
-
   catch(const char *e)
   {
-    error() << e << eom;
+    msg.error() << e << messaget::eom;
     return true;
   }
-
   catch(const std::string e)
   {
-    error() << e << eom;
+    msg.error() << e << messaget::eom;
     return true;
   }
-
   catch(int)
   {
     return true;
   }
-
   catch(std::bad_alloc)
   {
-    error() << "Out of memory" << eom;
+    msg.error() << "Out of memory" << messaget::eom;
     return true;
   }
 

src/goto-programs/get_goto_model.h

@@ -1,6 +1,6 @@
 /*******************************************************************\
 
-Module: Obtain a Goto Program
+Module: Initialize a Goto Program
 
 Author: Daniel Kroening, [email protected]
 
@@ -14,10 +14,9 @@ Author: Daniel Kroening, [email protected]
 
 #include "goto_model.h"
 
-class get_goto_modelt:public goto_modelt, public messaget
-{
-public:
-  bool operator()(const cmdlinet &);
-};
+bool initialize_goto_model(
+  goto_modelt &goto_model,
+  const cmdlinet &cmdline,
+  message_handlert &message_handler);
 
 #endif // CPROVER_GOTO_PROGRAMS_GET_GOTO_MODEL_H

src/symex/symex_parse_options.cpp

@@ -177,9 +177,7 @@ int symex_parse_optionst::doit()
 
   eval_verbosity();
 
-  goto_model.set_message_handler(get_message_handler());
-
-  if(goto_model(cmdline))
+  if(initialize_goto_model(goto_model, cmdline, get_message_handler()))
     return 6;
 
   if(process_goto_program(options))

src/symex/symex_parse_options.h

@@ -59,7 +59,7 @@ class symex_parse_optionst:
 
 protected:
   ui_message_handlert ui_message_handler;
-  get_goto_modelt goto_model;
+  goto_modelt goto_model;
 
   void get_command_line_options(optionst &options);
   bool process_goto_program(const optionst &options);