diffblue · kroening · Jan 22, 2017 · Jan 22, 2017 · Jan 22, 2017 · Jan 22, 2017
diff --git a/src/goto-cc/armcc_mode.cpp b/src/goto-cc/armcc_mode.cpp
@@ -59,8 +59,8 @@ int armcc_modet::doit()
   if(cmdline.isset("verbosity"))
     verbosity=unsafe_string2int(cmdline.get_value("verbosity"));
 
-  compiler.ui_message_handler.set_verbosity(verbosity);
-  ui_message_handler.set_verbosity(verbosity);
+  compiler.set_message_handler(get_message_handler());
+  message_handler.set_verbosity(verbosity);
 
   debug() << "ARM mode" << eom;
 

diff --git a/src/goto-cc/armcc_mode.h b/src/goto-cc/armcc_mode.h
@@ -11,25 +11,28 @@ Date: June 2006
 #ifndef CPROVER_GOTO_CC_ARMCC_MODE_H
 #define CPROVER_GOTO_CC_ARMCC_MODE_H
 
+#include <util/cout_message.h>
+
 #include "goto_cc_mode.h"
 #include "armcc_cmdline.h"
 
 class armcc_modet:public goto_cc_modet
 {
 public:
-  virtual int doit();
-  virtual void help_mode();
+  int doit() final;
+  void help_mode() final;
 
   armcc_modet(
     armcc_cmdlinet &_armcc_cmdline,
     const std::string &_base_name):
-    goto_cc_modet(_armcc_cmdline, _base_name),
+    goto_cc_modet(_armcc_cmdline, _base_name, message_handler),
     cmdline(_armcc_cmdline)
   {
   }
 
 protected:
   armcc_cmdlinet &cmdline;
+  gcc_message_handlert message_handler;
 };
 
 #endif // CPROVER_GOTO_CC_ARMCC_MODE_H
diff --git a/src/goto-cc/as_mode.cpp b/src/goto-cc/as_mode.cpp
@@ -22,6 +22,7 @@ Author: Michael Tautschnig
 #include <util/tempdir.h>
 #include <util/config.h>
 #include <util/get_base_name.h>
+#include <util/cout_message.h>
 
 #include <cbmc/version.h>
 
@@ -79,7 +80,7 @@ as_modet::as_modet(
   goto_cc_cmdlinet &_cmdline,
   const std::string &_base_name,
   bool _produce_hybrid_binary):
-  goto_cc_modet(_cmdline, _base_name),
+  goto_cc_modet(_cmdline, _base_name, message_handler),
   produce_hybrid_binary(_produce_hybrid_binary),
   native_tool_name(assembler_name(cmdline, base_name))
 {
@@ -137,7 +138,7 @@ int as_modet::doit()
   if(cmdline.isset("verbosity"))
     verbosity=unsafe_string2unsigned(cmdline.get_value("verbosity"));
 
-  ui_message_handler.set_verbosity(verbosity);
+  message_handler.set_verbosity(verbosity);
 
   if(act_as_as86)
   {

diff --git a/src/goto-cc/as_mode.h b/src/goto-cc/as_mode.h
@@ -11,6 +11,8 @@ Date: July 2016
 #ifndef CPROVER_GOTO_CC_AS_MODE_H
 #define CPROVER_GOTO_CC_AS_MODE_H
 
+#include <util/cout_message.h>
+
 #include "goto_cc_mode.h"
 
 class as_modet:public goto_cc_modet
@@ -22,10 +24,11 @@ class as_modet:public goto_cc_modet
   as_modet(
     goto_cc_cmdlinet &_cmdline,
     const std::string &_base_name,
-    bool _produce_hybrid_binar);
+    bool _produce_hybrid_binary);
 
 protected:
-  bool produce_hybrid_binary;
+  gcc_message_handlert message_handler;
+  const bool produce_hybrid_binary;
   const std::string native_tool_name;
 
   int run_as(); // call as with original command line

diff --git a/src/goto-cc/cw_mode.cpp b/src/goto-cc/cw_mode.cpp
@@ -59,8 +59,8 @@ int cw_modet::doit()
   if(cmdline.isset("verbosity"))
     verbosity=unsafe_string2unsigned(cmdline.get_value("verbosity"));
 
-  compiler.ui_message_handler.set_verbosity(verbosity);
-  ui_message_handler.set_verbosity(verbosity);
+  compiler.set_message_handler(get_message_handler());
+  message_handler.set_verbosity(verbosity);
 
   debug() << "CodeWarrior mode" << eom;
 

diff --git a/src/goto-cc/cw_mode.h b/src/goto-cc/cw_mode.h
@@ -11,6 +11,8 @@ Date: June 2006
 #ifndef CPROVER_GOTO_CC_CW_MODE_H
 #define CPROVER_GOTO_CC_CW_MODE_H
 
+#include <util/cout_message.h>
+
 #include "goto_cc_mode.h"
 #include "gcc_cmdline.h"
 
@@ -21,13 +23,14 @@ class cw_modet:public goto_cc_modet
   virtual void help_mode();
 
   cw_modet(gcc_cmdlinet &_gcc_cmdline, const std::string &_base_name):
-    goto_cc_modet(_gcc_cmdline, _base_name),
+    goto_cc_modet(_gcc_cmdline, _base_name, message_handler),
     cmdline(_gcc_cmdline)
   {
   }
 
 protected:
   gcc_cmdlinet &cmdline;
+  console_message_handlert message_handler;
 };
 
 #endif // CPROVER_GOTO_CC_CW_MODE_H
diff --git a/src/goto-cc/gcc_mode.cpp b/src/goto-cc/gcc_mode.cpp
@@ -121,7 +121,7 @@ gcc_modet::gcc_modet(
   goto_cc_cmdlinet &_cmdline,
   const std::string &_base_name,
   bool _produce_hybrid_binary):
-  goto_cc_modet(_cmdline, _base_name),
+  goto_cc_modet(_cmdline, _base_name, gcc_message_handler),
   produce_hybrid_binary(_produce_hybrid_binary),
   act_as_ld(base_name=="ld" ||
             base_name.find("goto-ld")!=std::string::npos)
@@ -223,7 +223,7 @@ int gcc_modet::doit()
   if(cmdline.isset("verbosity"))
     verbosity=unsafe_string2unsigned(cmdline.get_value("verbosity"));
 
-  ui_message_handler.set_verbosity(verbosity);
+  gcc_message_handler.set_verbosity(verbosity);
 
   if(act_as_ld)
   {
@@ -303,7 +303,7 @@ int gcc_modet::doit()
 
   // determine actions to be undertaken
   compilet compiler(cmdline);
-  compiler.ui_message_handler.set_verbosity(verbosity);
+  compiler.set_message_handler(get_message_handler());
 
   if(act_as_ld)
     compiler.mode=compilet::LINK_LIBRARY;

diff --git a/src/goto-cc/gcc_mode.h b/src/goto-cc/gcc_mode.h
@@ -11,25 +11,29 @@ Date: June 2006
 #ifndef CPROVER_GOTO_CC_GCC_MODE_H
 #define CPROVER_GOTO_CC_GCC_MODE_H
 
+#include <util/cout_message.h>
+
 #include "goto_cc_mode.h"
 
 class gcc_modet:public goto_cc_modet
 {
 public:
-  virtual int doit();
-  virtual void help_mode();
+  int doit() final;
+  void help_mode() final;
 
   gcc_modet(
     goto_cc_cmdlinet &_cmdline,
     const std::string &_base_name,
     bool _produce_hybrid_binary);
 
 protected:
+  gcc_message_handlert gcc_message_handler;
+
   const bool produce_hybrid_binary;
 
   const bool act_as_ld;
   std::string native_tool_name;
-
+  
   int preprocess(
     const std::string &language,
     const std::string &src,

diff --git a/src/goto-cc/goto_cc_mode.cpp b/src/goto-cc/goto_cc_mode.cpp
@@ -35,11 +35,11 @@ Function: goto_cc_modet::goto_cc_modet
 
 goto_cc_modet::goto_cc_modet(
   goto_cc_cmdlinet &_cmdline,
-  const std::string &_base_name):
-  language_uit(_cmdline, ui_message_handler),
-  ui_message_handler(_cmdline, "goto-cc " CBMC_VERSION),
-  base_name(_base_name),
-  cmdline(_cmdline)
+  const std::string &_base_name,
+  message_handlert &_message_handler):
+  messaget(_message_handler),
+  cmdline(_cmdline),
+  base_name(_base_name)
 {
   register_languages();
 }

diff --git a/src/goto-cc/goto_cc_mode.h b/src/goto-cc/goto_cc_mode.h
@@ -15,7 +15,7 @@ Date: June 2006
 
 #include "goto_cc_cmdline.h"
 
-class goto_cc_modet:public language_uit
+class goto_cc_modet:public messaget
 {
 public:
   virtual int main(int argc, const char **argv);
@@ -25,15 +25,15 @@ class goto_cc_modet:public language_uit
   virtual void usage_error();
 
   goto_cc_modet(
-    goto_cc_cmdlinet &_cmdline,
-    const std::string &_base_name);
+    goto_cc_cmdlinet &,
+    const std::string &_base_name,
+    message_handlert &);
   ~goto_cc_modet();
 
 protected:
-  ui_message_handlert ui_message_handler;
+  goto_cc_cmdlinet &cmdline;
   const std::string base_name;
   void register_languages();
-  goto_cc_cmdlinet &cmdline;
 };
 
 #endif // CPROVER_GOTO_CC_GOTO_CC_MODE_H