Pass message handler on to compilet

GOTO conversion must honour the message handler set up by the chosen goto-cc
mode. Thus the message handler set up in the specific mode has to be handed on
to compilet. As a language_uit this requires a ui_message_handlert. Consequently
make console_message_handlert, gcc_message_handlert ui_message_handlert in PLAIN
ui mode (which is consistent).

Author: tautschnig

regression/ansi-c/message_handling1/main.c

@@ -0,0 +1,9 @@
+int main()
+{
+  goto bla;
+
+  for(int i=0; i<5; ++i)
+  {
+bla: i=10;
+  }
+}

regression/ansi-c/message_handling1/test.desc

@@ -0,0 +1,7 @@
+CORE
+main.c
+--verbosity 2
+^EXIT=0$
+^SIGNAL=0$
+--
+encountered goto `bla' that enters one or more lexical blocks

src/goto-cc/armcc_mode.cpp

@@ -46,7 +46,7 @@ int armcc_modet::doit()
 
   unsigned int verbosity=1;
 
-  compilet compiler(cmdline, cmdline.isset("diag_error="));
+  compilet compiler(cmdline, message_handler, cmdline.isset("diag_error="));
 
   #if 0
   bool act_as_ld=

src/goto-cc/as_mode.cpp

@@ -159,8 +159,7 @@ int as_modet::doit()
   config.set(cmdline);
 
   // determine actions to be undertaken
-  compilet compiler(cmdline, cmdline.isset("fatal-warnings"));
-  compiler.ui_message_handler.set_verbosity(verbosity);
+  compilet compiler(cmdline, message_handler, cmdline.isset("fatal-warnings"));
 
   if(cmdline.isset('b')) // as86 only
   {

src/goto-cc/compile.cpp

@@ -415,7 +415,7 @@ bool compilet::link()
     symbol_table.remove(goto_functionst::entry_point());
     compiled_functions.function_map.erase(goto_functionst::entry_point());
 
-    if(ansi_c_entry_point(symbol_table, "main", ui_message_handler))
+    if(ansi_c_entry_point(symbol_table, "main", get_message_handler()))
       return true;
 
     // entry_point may (should) add some more functions.
@@ -758,9 +758,8 @@ Function: compilet::compilet
 
 \*******************************************************************/
 
-compilet::compilet(cmdlinet &_cmdline, bool Werror):
-  language_uit(_cmdline, ui_message_handler),
-  ui_message_handler(_cmdline, "goto-cc " CBMC_VERSION),
+compilet::compilet(cmdlinet &_cmdline, ui_message_handlert &mh, bool Werror):
+  language_uit(_cmdline, mh),
   ns(symbol_table),
   cmdline(_cmdline),
   warning_is_fatal(Werror)
@@ -849,7 +848,7 @@ Function: compilet::convert_symbols
 
 void compilet::convert_symbols(goto_functionst &dest)
 {
-  goto_convert_functionst converter(symbol_table, dest, ui_message_handler);
+  goto_convert_functionst converter(symbol_table, dest, get_message_handler());
 
   // the compilation may add symbols!
 

src/goto-cc/compile.h

@@ -20,7 +20,6 @@ Date: June 2006
 class compilet:public language_uit
 {
 public:
-  ui_message_handlert ui_message_handler;
   namespacet ns;
   goto_functionst compiled_functions;
   bool echo_file_name;
@@ -45,7 +44,7 @@ class compilet:public language_uit
   std::string object_file_extension;
   std::string output_file_object, output_file_executable;
 
-  compilet(cmdlinet &_cmdline, bool Werror);
+  compilet(cmdlinet &_cmdline, ui_message_handlert &mh, bool Werror);
 
   ~compilet();
 

src/goto-cc/cw_mode.cpp

@@ -46,7 +46,7 @@ int cw_modet::doit()
 
   unsigned int verbosity=1;
 
-  compilet compiler(cmdline, cmdline.isset("Werror"));
+  compilet compiler(cmdline, message_handler, cmdline.isset("Werror"));
 
   #if 0
   bool act_as_ld=

src/goto-cc/gcc_mode.cpp

@@ -304,10 +304,10 @@ int gcc_modet::doit()
 
   // determine actions to be undertaken
   compilet compiler(cmdline,
+                    gcc_message_handler,
                     cmdline.isset("Werror") &&
                     cmdline.isset("Wextra") &&
                     !cmdline.isset("Wno-error"));
-  compiler.set_message_handler(get_message_handler());
 
   if(act_as_ld)
     compiler.mode=compilet::LINK_LIBRARY;

src/goto-cc/ms_cl_mode.cpp

@@ -59,7 +59,7 @@ int ms_cl_modet::doit()
 
   unsigned int verbosity=1;
 
-  compilet compiler(cmdline, cmdline.isset("WX"));
+  compilet compiler(cmdline, message_handler, cmdline.isset("WX"));
 
   #if 0
   bool act_as_ld=

src/langapi/language_ui.cpp

@@ -33,8 +33,8 @@ Function: language_uit::language_uit
 language_uit::language_uit(
   const cmdlinet &cmdline,
   ui_message_handlert &_ui_message_handler):
-  ui_message_handler(_ui_message_handler),
-  _cmdline(cmdline)
+  _cmdline(cmdline),
+  ui_message_handler(_ui_message_handler)
 {
   set_message_handler(ui_message_handler);
 }

src/langapi/language_ui.h

@@ -48,10 +48,9 @@ class language_uit:public messaget
     return ui_message_handler.get_ui();
   }
 
-  ui_message_handlert &ui_message_handler;
-
 protected:
   const cmdlinet &_cmdline;
+  ui_message_handlert &ui_message_handler;
 };
 
 #endif // CPROVER_LANGAPI_LANGUAGE_UI_H

src/util/cout_message.h

@@ -9,7 +9,7 @@ Author: Daniel Kroening, [email protected]
 #ifndef CPROVER_UTIL_COUT_MESSAGE_H
 #define CPROVER_UTIL_COUT_MESSAGE_H
 
-#include "message.h"
+#include "ui_message.h"
 
 class cout_message_handlert:public stream_message_handlert
 {
@@ -25,7 +25,7 @@ class cerr_message_handlert:public stream_message_handlert
   cerr_message_handlert();
 };
 
-class console_message_handlert:public message_handlert
+class console_message_handlert:public ui_message_handlert
 {
 public:
   // level 4 and upwards go to cout, level 1-3 to cerr
@@ -36,7 +36,7 @@ class console_message_handlert:public message_handlert
   virtual void flush(unsigned level) override;
 };
 
-class gcc_message_handlert:public message_handlert
+class gcc_message_handlert:public ui_message_handlert
 {
 public:
   // aims to imitate the messages gcc prints

src/util/ui_message.h

@@ -18,6 +18,10 @@ class ui_message_handlert:public message_handlert
 
   ui_message_handlert(uit, const std::string &program);
   ui_message_handlert(const class cmdlinet &, const std::string &program);
+  ui_message_handlert():
+    _ui(uit::PLAIN)
+  {
+  }
 
   virtual ~ui_message_handlert();