messaget formatting manipulators are now static data members

Author: Daniel Kroening

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

@@ -71,9 +71,15 @@ 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.

src/util/message.h

@@ -303,40 +303,22 @@ class messaget
 
   /// return to default formatting,
   /// as defined by the terminal
-  static commandt reset()
-  {
-    return command(0);
-  }
+  static const commandt reset;
 
   /// render text with red foreground color
-  static commandt red()
-  {
-    return command(31);
-  }
+  static const commandt red;
 
   /// render text with green foreground color
-  static commandt green()
-  {
-    return command(32);
-  }
+  static const commandt green;
 
   /// render text with yellow foreground color
-  static commandt yellow()
-  {
-    return command(33);
-  }
+  static const commandt yellow;
 
   /// render text with blue foreground color
-  static commandt blue()
-  {
-    return command(34);
-  }
+  static const commandt blue;
 
   /// render text with bold font
-  static commandt bold()
-  {
-    return command(1);
-  }
+  static const commandt bold;
 
   /// render text with faint font
   static const commandt faint;