Add preformatted message flag

This allows users of a message handler to note they have already formatted a particular message according to its output conventions (currently XML or JSON) and so output something more complicated than it can synthesise on its own.
smowton · Jun 26, 2017 · 20e4def · 20e4def
1 parent 9ac5dff
commit 20e4def
Show file tree

Hide file tree

Showing 7 changed files with 96 additions and 42 deletions.
diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp
@@ -66,7 +66,7 @@ void bmct::error_trace()
     {
       xmlt xml;
       convert(ns, goto_trace, xml);
-      status() << xml << eom;
+      status() << preformatted_output << xml << eom;
     }
     break;
 
@@ -83,7 +83,7 @@ void bmct::error_trace()
       result["status"]=json_stringt("failed");
       jsont &json_trace=result["trace"];
       convert(ns, goto_trace, json_trace);
-      status() << ",\n" << json_result << eom;
+      status() << preformatted_output << json_result << eom;
     }
     break;
   }

diff --git a/src/util/cout_message.cpp b/src/util/cout_message.cpp
@@ -31,9 +31,10 @@ cerr_message_handlert::cerr_message_handlert():
 
 void console_message_handlert::print(
   unsigned level,
-  const std::string &message)
+  const std::string &message,
+  bool preformatted)
 {
-  message_handlert::print(level, message);
+  message_handlert::print(level, message, preformatted);
 
   if(verbosity<level)
     return;
@@ -101,7 +102,8 @@ void gcc_message_handlert::print(
   unsigned level,
   const std::string &message,
   int sequence_number,
-  const source_locationt &location)
+  const source_locationt &location,
+  bool preformatted)
 {
   const irep_idt file=location.get_file();
   const irep_idt line=location.get_line();
@@ -139,14 +141,15 @@ void gcc_message_handlert::print(
 
   dest+=message;
 
-  print(level, dest);
+  print(level, dest, preformatted);
 }
 
 void gcc_message_handlert::print(
   unsigned level,
-  const std::string &message)
+  const std::string &message,
+  bool preformatted)
 {
-  message_handlert::print(level, message);
+  message_handlert::print(level, message, preformatted);
 
   // gcc appears to send everything to cerr
   if(verbosity>=level)

diff --git a/src/util/cout_message.h b/src/util/cout_message.h
@@ -32,7 +32,8 @@ class console_message_handlert:public ui_message_handlert
   // level 4 and upwards go to cout, level 1-3 to cerr
   virtual void print(
     unsigned level,
-    const std::string &message) override;
+    const std::string &message,
+    bool preformatted) override;
 
   virtual void flush(unsigned level) override;
 };
@@ -43,13 +44,15 @@ class gcc_message_handlert:public ui_message_handlert
   // aims to imitate the messages gcc prints
   virtual void print(
     unsigned level,
-    const std::string &message) override;
+    const std::string &message,
+    bool preformatted) override;
 
   virtual void print(
     unsigned level,
     const std::string &message,
     int sequence_number,
-    const source_locationt &location) override;
+    const source_locationt &location,
+    bool preformatted) override;
 };
 
 #endif // CPROVER_UTIL_COUT_MESSAGE_H
diff --git a/src/util/message.cpp b/src/util/message.cpp
@@ -13,7 +13,8 @@ void message_handlert::print(
   unsigned level,
   const std::string &message,
   int sequence_number,
-  const source_locationt &location)
+  const source_locationt &location,
+  bool preformatted)
 {
   std::string dest;
 
@@ -51,12 +52,13 @@ void message_handlert::print(
     dest+=": ";
   dest+=message;
 
-  print(level, dest);
+  print(level, dest, preformatted);
 }
 
 void message_handlert::print(
   unsigned level,
-  const std::string &message)
+  const std::string &message,
+  bool preformatted)
 {
   if(level>=message_count.size())
     message_count.resize(level+1, 0);

diff --git a/src/util/message.h b/src/util/message.h
@@ -23,13 +23,17 @@ class message_handlert
   {
   }
 
-  virtual void print(unsigned level, const std::string &message) = 0;
+  virtual void print(
+    unsigned level,
+    const std::string &message,
+    bool preformatted) = 0;
 
   virtual void print(
     unsigned level,
     const std::string &message,
     int sequence_number,
-    const source_locationt &location);
+    const source_locationt &location,
+    bool preformatted);
 
   virtual void flush(unsigned level)
   {
@@ -59,18 +63,22 @@ class message_handlert
 class null_message_handlert:public message_handlert
 {
 public:
-  virtual void print(unsigned level, const std::string &message)
+  virtual void print(
+    unsigned level,
+    const std::string &message,
+    bool preformatted)
   {
-    message_handlert::print(level, message);
+    message_handlert::print(level, message, preformatted);
   }
 
   virtual void print(
     unsigned level,
     const std::string &message,
     int sequence_number,
-    const source_locationt &location)
+    const source_locationt &location,
+    bool preformatted)
   {
-    print(level, message);
+    print(level, message, preformatted);
   }
 };
 
@@ -81,9 +89,12 @@ class stream_message_handlert:public message_handlert
   {
   }
 
-  virtual void print(unsigned level, const std::string &message)
+  virtual void print(
+    unsigned level,
+    const std::string &message,
+    bool preformatted)
   {
-    message_handlert::print(level, message);
+    message_handlert::print(level, message, preformatted);
 
     if(verbosity>=level)
       out << message << '\n';
@@ -157,20 +168,23 @@ class messaget
       unsigned _message_level,
       messaget &_message):
       message_level(_message_level),
-      message(_message)
+      message(_message),
+      preformatted(false)
     {
     }
 
     mstreamt(const mstreamt &other):
       message_level(other.message_level),
       message(other.message),
-      source_location(other.source_location)
+      source_location(other.source_location),
+      preformatted(false)
     {
     }
 
     unsigned message_level;
     messaget &message;
     source_locationt source_location;
+    bool preformatted;
 
     template <class T>
     mstreamt &operator << (const T &x)
@@ -196,15 +210,23 @@ class messaget
         m.message_level,
         m.str(),
         -1,
-        m.source_location);
+        m.source_location,
+        m.preformatted);
       m.message.message_handler->flush(m.message_level);
     }
+    m.preformatted=false;
     m.clear(); // clears error bits
     m.str(std::string()); // clears the string
     m.source_location.clear();
     return m;
   }
 
+  static mstreamt &preformatted_output(mstreamt &m)
+  {
+    m.preformatted=true;
+    return m;
+  }
+
   // in lieu of std::endl
   static mstreamt &endl(mstreamt &m)
   {

diff --git a/src/util/ui_message.cpp b/src/util/ui_message.cpp
@@ -89,7 +89,8 @@ const char *ui_message_handlert::level_string(unsigned level)
 
 void ui_message_handlert::print(
   unsigned level,
-  const std::string &message)
+  const std::string &message,
+  bool preformatted)
 {
   if(verbosity>=level)
   {
@@ -98,7 +99,7 @@ void ui_message_handlert::print(
     case uit::PLAIN:
     {
       console_message_handlert console_message_handler;
-      console_message_handler.print(level, message);
+      console_message_handler.print(level, message, preformatted);
     }
     break;
 
@@ -107,7 +108,7 @@ void ui_message_handlert::print(
     {
       source_locationt location;
       location.make_nil();
-      print(level, message, -1, location);
+      print(level, message, -1, location, preformatted);
     }
     break;
     }
@@ -118,17 +119,18 @@ void ui_message_handlert::print(
   unsigned level,
   const std::string &message,
   int sequence_number,
-  const source_locationt &location)
+  const source_locationt &location,
+  bool preformatted)
 {
-  message_handlert::print(level, message);
+  message_handlert::print(level, message, preformatted);
 
   if(verbosity>=level)
   {
     switch(get_ui())
     {
     case uit::PLAIN:
       message_handlert::print(
-        level, message, sequence_number, location);
+        level, message, sequence_number, location, preformatted);
       break;
 
     case uit::XML_UI:
@@ -144,7 +146,7 @@ void ui_message_handlert::print(
       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, sequence_number_str, location, preformatted);
     }
     break;
     }
@@ -155,19 +157,20 @@ void ui_message_handlert::ui_msg(
   const std::string &type,
   const std::string &msg1,
   const std::string &msg2,
-  const source_locationt &location)
+  const source_locationt &location,
+  bool preformatted)
 {
   switch(get_ui())
   {
   case uit::PLAIN:
     break;
 
   case uit::XML_UI:
-    xml_ui_msg(type, msg1, msg2, location);
+    xml_ui_msg(type, msg1, msg2, location, preformatted);
     break;
 
   case uit::JSON_UI:
-    json_ui_msg(type, msg1, msg2, location);
+    json_ui_msg(type, msg1, msg2, location, preformatted);
     break;
   }
 }
@@ -176,8 +179,16 @@ void ui_message_handlert::xml_ui_msg(
   const std::string &type,
   const std::string &msg1,
   const std::string &msg2,
-  const source_locationt &location)
+  const source_locationt &location,
+  bool preformatted)
 {
+  if(preformatted)
+  {
+    // Expect the message is already an XML fragment.
+    std::cout << msg1 << '\n';
+    return;
+  }
+
   xmlt result;
   result.name="message";
 
@@ -196,8 +207,16 @@ void ui_message_handlert::json_ui_msg(
   const std::string &type,
   const std::string &msg1,
   const std::string &msg2,
-  const source_locationt &location)
+  const source_locationt &location,
+  bool preformatted)
 {
+  if(preformatted)
+  {
+    // Expect the message is already a JSON fragment.
+    std::cout << ",\n" << msg1;
+    return;
+  }
+
   json_objectt result;
 
   #if 0

diff --git a/src/util/ui_message.h b/src/util/ui_message.h
@@ -44,32 +44,37 @@ class ui_message_handlert:public message_handlert
   // overloading
   virtual void print(
     unsigned level,
-    const std::string &message);
+    const std::string &message,
+    bool preformatted);
 
   // overloading
   virtual void print(
     unsigned level,
     const std::string &message,
     int sequence_number,
-    const source_locationt &location);
+    const source_locationt &location,
+    bool preformatted);
 
   virtual void xml_ui_msg(
     const std::string &type,
     const std::string &msg1,
     const std::string &msg2,
-    const source_locationt &location);
+    const source_locationt &location,
+    bool preformatted);
 
   virtual void json_ui_msg(
     const std::string &type,
     const std::string &msg1,
     const std::string &msg2,
-    const source_locationt &location);
+    const source_locationt &location,
+    bool preformatted);
 
   virtual void ui_msg(
     const std::string &type,
     const std::string &msg1,
     const std::string &msg2,
-    const source_locationt &location);
+    const source_locationt &location,
+    bool preformatted);
 
   const char *level_string(unsigned level);
 };