Merge pull request #2747 from diffblue/cleanup-message-handler

Cleanup message handler

Author: kroening

src/util/cout_message.cpp

@@ -100,7 +100,6 @@ void console_message_handlert::flush(unsigned level)
 void gcc_message_handlert::print(
   unsigned level,
   const std::string &message,
-  int,
   const source_locationt &location)
 {
   const irep_idt file=location.get_file();

src/util/cout_message.h

@@ -60,7 +60,6 @@ class gcc_message_handlert:public ui_message_handlert
   virtual void print(
     unsigned level,
     const std::string &message,
-    int sequence_number,
     const source_locationt &location) override;
 };
 

src/util/message.cpp

@@ -14,7 +14,6 @@ Author: Daniel Kroening, [email protected]
 void message_handlert::print(
   unsigned level,
   const std::string &message,
-  int,
   const source_locationt &location)
 {
   std::string dest;
@@ -92,7 +91,6 @@ unsigned messaget::eval_verbosity(
         messaget::M_WARNING,
         "verbosity value " + user_input + " out of range, using debug-level (" +
           std::to_string(messaget::M_DEBUG) + ") verbosity",
-        -1,
         source_locationt());
 
       v = messaget::M_DEBUG;

src/util/message.h

@@ -50,7 +50,6 @@ class message_handlert
   virtual void print(
     unsigned level,
     const std::string &message,
-    int sequence_number,
     const source_locationt &location);
 
   virtual void flush(unsigned level)
@@ -65,7 +64,7 @@ class message_handlert
   void set_verbosity(unsigned _verbosity) { verbosity=_verbosity; }
   unsigned get_verbosity() const { return verbosity; }
 
-  unsigned get_message_count(unsigned level) const
+  std::size_t get_message_count(unsigned level) const
   {
     if(level>=message_count.size())
       return 0;
@@ -75,7 +74,7 @@ class message_handlert
 
 protected:
   unsigned verbosity;
-  std::vector<unsigned> message_count;
+  std::vector<std::size_t> message_count;
 };
 
 class null_message_handlert:public message_handlert
@@ -89,7 +88,6 @@ class null_message_handlert:public message_handlert
   virtual void print(
     unsigned level,
     const std::string &message,
-    int,
     const source_locationt &)
   {
     print(level, message);
@@ -276,7 +274,6 @@ class messaget
       m.message.message_handler->print(
         m.message_level,
         m.str(),
-        -1,
         m.source_location);
       m.message.message_handler->flush(m.message_level);
     }

src/util/ui_message.cpp

@@ -149,7 +149,7 @@ void ui_message_handlert::print(
     {
       source_locationt location;
       location.make_nil();
-      print(level, message, -1, location);
+      print(level, message, location);
       if(always_flush)
         flush(level);
     }
@@ -206,7 +206,6 @@ void ui_message_handlert::print(
 void ui_message_handlert::print(
   unsigned level,
   const std::string &message,
-  int sequence_number,
   const source_locationt &location)
 {
   message_handlert::print(level, message);
@@ -217,7 +216,7 @@ void ui_message_handlert::print(
     {
     case uit::PLAIN:
       message_handlert::print(
-        level, message, sequence_number, location);
+        level, message, location);
       break;
 
     case uit::XML_UI:
@@ -230,10 +229,7 @@ void ui_message_handlert::print(
 
       const char *type=level_string(level);
 
-      std::string sequence_number_str=
-        sequence_number>=0?std::to_string(sequence_number):"";
-
-      ui_msg(type, tmp_message, sequence_number_str, location);
+      ui_msg(type, tmp_message, location);
     }
     break;
     }
@@ -242,8 +238,7 @@ void ui_message_handlert::print(
 
 void ui_message_handlert::ui_msg(
   const std::string &type,
-  const std::string &msg1,
-  const std::string &msg2,
+  const std::string &msg,
   const source_locationt &location)
 {
   switch(get_ui())
@@ -252,19 +247,18 @@ void ui_message_handlert::ui_msg(
     break;
 
   case uit::XML_UI:
-    xml_ui_msg(type, msg1, msg2, location);
+    xml_ui_msg(type, msg, location);
     break;
 
   case uit::JSON_UI:
-    json_ui_msg(type, msg1, msg2, location);
+    json_ui_msg(type, msg, location);
     break;
   }
 }
 
 void ui_message_handlert::xml_ui_msg(
   const std::string &type,
   const std::string &msg1,
-  const std::string &,
   const source_locationt &location)
 {
   xmlt result;
@@ -287,7 +281,6 @@ void ui_message_handlert::xml_ui_msg(
 void ui_message_handlert::json_ui_msg(
   const std::string &type,
   const std::string &msg1,
-  const std::string &,
   const source_locationt &location)
 {
   INVARIANT(json_stream, "JSON stream must be initialized before use");

src/util/ui_message.h

@@ -71,7 +71,6 @@ class ui_message_handlert : public message_handlert
   virtual void print(
     unsigned level,
     const std::string &message,
-    int sequence_number,
     const source_locationt &location) override;
 
   virtual void print(
@@ -84,20 +83,17 @@ class ui_message_handlert : public message_handlert
 
   virtual void xml_ui_msg(
     const std::string &type,
-    const std::string &msg1,
-    const std::string &msg2,
+    const std::string &msg,
     const source_locationt &location);
 
   virtual void json_ui_msg(
     const std::string &type,
-    const std::string &msg1,
-    const std::string &msg2,
+    const std::string &msg,
     const source_locationt &location);
 
   virtual void ui_msg(
     const std::string &type,
-    const std::string &msg1,
-    const std::string &msg2,
+    const std::string &msg,
     const source_locationt &location);
 
   const char *level_string(unsigned level);