mstreamt manipulators are now static

src/cbmc/all_properties.cpp

@@ -164,11 +164,11 @@ void bmc_all_propertiest::report(const cover_goalst &cover_goals)
                  << goal_pair.second.description << ": ";
 
         if(goal_pair.second.status == goalt::statust::SUCCESS)
-          result() << green();
+          result() << green;
         else
-          result() << red();
+          result() << red;
 
-        result() << goal_pair.second.status_string() << reset() << eom;
+        result() << goal_pair.second.status_string() << reset << eom;
       }
 
       if(bmc.options.get_bool_option("trace"))

src/cbmc/bmc.cpp

@@ -153,7 +153,7 @@ bmct::run_decision_procedure(prop_convt &prop_conv)
 
 void bmct::report_success()
 {
-  result() << bold() << "VERIFICATION SUCCESSFUL" << reset() << eom;
+  result() << bold << "VERIFICATION SUCCESSFUL" << reset << eom;
 
   switch(ui_message_handler.get_ui())
   {
@@ -180,7 +180,7 @@ void bmct::report_success()
 
 void bmct::report_failure()
 {
-  result() << bold() << "VERIFICATION FAILED" << reset() << eom;
+  result() << bold << "VERIFICATION FAILED" << reset << eom;
 
   switch(ui_message_handler.get_ui())
   {

src/goto-analyzer/static_verifier.cpp

@@ -232,22 +232,22 @@ bool static_verifier(
 
         if(e.is_true())
         {
-          m.result() << m.green() << "Success" << m.reset();
+          m.result() << m.green << "Success" << m.reset;
           pass++;
         }
         else if(e.is_false())
         {
-          m.result() << m.red() << "Failure" << m.reset() << " (if reachable)";
+          m.result() << m.red << "Failure" << m.reset << " (if reachable)";
           fail++;
         }
         else if(domain.is_bottom())
         {
-          m.result() << m.green() << "Success" << m.reset() << " (unreachable)";
+          m.result() << m.green << "Success" << m.reset << " (unreachable)";
           pass++;
         }
         else
         {
-          m.result() << m.yellow() << "Unknown" << m.reset();
+          m.result() << m.yellow << "Unknown" << m.reset;
           unknown++;
         }
 
@@ -258,11 +258,11 @@ bool static_verifier(
     }
   }
 
-  m.status() << m.bold() << "Summary: "
+  m.status() << m.bold << "Summary: "
              << pass << " pass, "
              << fail << " fail if reachable, "
              << unknown << " unknown"
-             << m.reset() << messaget::eom;
+             << m.reset << messaget::eom;
 
   return false;
 }

src/util/message.cpp

@@ -68,6 +68,19 @@ messaget::~messaget()
 {
 }
 
+// Visual studio requires this (empty) static object
+messaget::eomt messaget::eom;
+
+const messaget::commandt messaget::reset(0);
+const messaget::commandt messaget::bold(1);
+const messaget::commandt messaget::faint(2);
+const messaget::commandt messaget::italic(3);
+const messaget::commandt messaget::underline(4);
+const messaget::commandt messaget::red(31);
+const messaget::commandt messaget::green(32);
+const messaget::commandt messaget::yellow(33);
+const messaget::commandt messaget::blue(34);
+
 /// Parse a (user-)provided string as a verbosity level and set it as the
 /// verbosity of dest.
 /// \param user_input  Input string; if empty, the default verbosity is used.

src/util/message.h

@@ -240,12 +240,6 @@ class messaget
       return *this;
     }
 
-    // for feeding in manipulator functions such as eom
-    mstreamt &operator << (mstreamt &(*func)(mstreamt &))
-    {
-      return func(*this);
-    }
-
   private:
     void assign_from(const mstreamt &other)
     {
@@ -257,9 +251,15 @@ class messaget
     friend class messaget;
   };
 
-  // Feeding 'eom' into the stream triggers
-  // the printing of the message
-  static mstreamt &eom(mstreamt &m)
+  // Feeding 'eom' into the stream triggers the printing of the message
+  // This is implemented as an I/O manipulator (compare to STL's endl).
+  class eomt
+  {
+  };
+
+  static eomt eom;
+
+  friend mstreamt &operator<<(mstreamt &m, eomt)
   {
     if(m.message.message_handler)
     {
@@ -275,58 +275,59 @@ class messaget
     return m;
   }
 
-  // in lieu of std::endl
-  static mstreamt &endl(mstreamt &m)
+  // This is an I/O manipulator (compare to STL's set_precision).
+  class commandt
   {
-    static_cast<std::ostream &>(m) << std::endl;
-    return m;
+  public:
+    explicit commandt(unsigned _command) : command(_command)
+    {
+    }
+
+    unsigned command;
+  };
+
+  /// feed a command into an mstreamt
+  friend mstreamt &operator<<(mstreamt &m, const commandt &c)
+  {
+    if(m.message.message_handler)
+      return m << m.message.message_handler->command(c.command);
+    else
+      return m;
   }
 
   /// \brief Create an ECMA-48 SGR (Select Graphic Rendition) command.
-  std::string command(unsigned c) const
+  static commandt command(unsigned c)
   {
-    if(message_handler)
-      return message_handler->command(c);
-    else
-      return std::string();
+    return commandt(c);
   }
 
   /// return to default formatting,
   /// as defined by the terminal
-  std::string reset() const
-  {
-    return command(0);
-  }
+  static const commandt reset;
 
   /// render text with red foreground color
-  std::string red() const
-  {
-    return command(31);
-  }
+  static const commandt red;
 
   /// render text with green foreground color
-  std::string green() const
-  {
-    return command(32);
-  }
+  static const commandt green;
 
   /// render text with yellow foreground color
-  std::string yellow() const
-  {
-    return command(33);
-  }
+  static const commandt yellow;
 
   /// render text with blue foreground color
-  std::string blue() const
-  {
-    return command(34);
-  }
+  static const commandt blue;
 
   /// render text with bold font
-  std::string bold() const
-  {
-    return command(1);
-  }
+  static const commandt bold;
+
+  /// render text with faint font
+  static const commandt faint;
+
+  /// render italic text
+  static const commandt italic;
+
+  /// render underlined text
+  static const commandt underline;
 
   mstreamt &get_mstream(unsigned message_level) const
   {