Fix messaget's copy-constructor and operator=

These were broken, leaving an mstreamt whose back-pointer pointed
into a different messaget than the one it enclosed, which could then have
its message_handlert changed with unexpected side-effects, or be deleted
causing a probable segfault on next log message.

The added unit tests verify that this no longer happens.

scripts/cpplint.py

@@ -4876,7 +4876,9 @@ def CheckStyle(filename, clean_lines, linenum, file_extension, nesting_state,
   CheckCommaSpacing(filename, clean_lines, linenum, error)
   CheckBracesSpacing(filename, clean_lines, linenum, nesting_state, error)
   CheckSpacingForFunctionCall(filename, clean_lines, linenum, error)
-  CheckCheck(filename, clean_lines, linenum, error)
+  # Disabled because whatever CHECK macro this was looking for, it isn't the
+  # CHECK macro used in Catch, but was complaining about it anyway.
+  #CheckCheck(filename, clean_lines, linenum, error)
   CheckAltTokens(filename, clean_lines, linenum, error)
   CheckAssert(filename, clean_lines, linenum, error)
   classinfo = nesting_state.InnermostClass()

src/solvers/refinement/string_refinement.cpp

@@ -145,7 +145,7 @@ string_refinementt::string_refinementt(const infot &info):
 
 /// display the current index set, for debugging
 static void display_index_set(
-  messaget::mstreamt stream,
+  messaget::mstreamt &stream,
   const namespacet &ns,
   const index_set_pairt &index_set)
 {

src/util/message.h

@@ -154,10 +154,17 @@ public:
 
   messaget(const messaget &other):
     message_handler(other.message_handler),
-    mstream(other.mstream)
+    mstream(other.mstream, *this)
   {
   }
 
+  messaget &operator=(const messaget &other)
+  {
+    message_handler=other.message_handler;
+    mstream.assign_from(other.mstream);
+    return *this;
+  }
+
   explicit messaget(message_handlert &_message_handler):
     message_handler(&_message_handler),
     mstream(M_DEBUG, *this)
@@ -177,13 +184,17 @@ public:
     {
     }
 
-    mstreamt(const mstreamt &other):
+    mstreamt(const mstreamt &other)=delete;
+
+    mstreamt(const mstreamt &other, messaget &_message):
       message_level(other.message_level),
-      message(other.message),
+      message(_message),
       source_location(other.source_location)
     {
     }
 
+    mstreamt &operator=(const mstreamt &other)=delete;
+
     unsigned message_level;
     messaget &message;
     source_locationt source_location;
@@ -220,6 +231,16 @@ public:
     {
       return func(*this);
     }
+
+  private:
+    void assign_from(const mstreamt &other)
+    {
+      message_level=other.message_level;
+      source_location=other.source_location;
+      // message, the pointer to my enclosing messaget, remains unaltered.
+    }
+
+    friend class messaget;
   };
 
   // Feeding 'eom' into the stream triggers

unit/Makefile

@@ -27,6 +27,7 @@ SRC += unit_tests.cpp \
        solvers/refinement/string_refinement/substitute_array_list.cpp \
        util/expr_cast/expr_cast.cpp \
        util/expr_iterator.cpp \
+       util/message.cpp \
        util/simplify_expr.cpp \
        catch_example.cpp \
        # Empty last line

unit/util/message.cpp

@@ -0,0 +1,51 @@
+/*******************************************************************\
+
+ Module: Messaget tests
+
+ Author: Diffblue Limited. All rights reserved.
+
+\*******************************************************************/
+
+#include <testing-utils/catch.hpp>
+#include <util/message.h>
+#include <sstream>
+#include <string.h>
+
+TEST_CASE("Copy a messaget")
+{
+  std::ostringstream sstream1, sstream2;
+  stream_message_handlert handler1(sstream1), handler2(sstream2);
+
+  messaget msg1(handler1);
+
+  // Copy messaget:
+  messaget msg2(msg1);
+
+  // Change its handler:
+  msg2.set_message_handler(handler2);
+
+  msg2.status() << "Test" << messaget::eom;
+
+  CHECK(sstream1.str()=="");
+  CHECK(sstream2.str()=="Test\n");
+}
+
+TEST_CASE("Assign a messaget")
+{
+  std::ostringstream sstream1, sstream2;
+  stream_message_handlert handler1(sstream1), handler2(sstream2);
+
+  messaget msg1(handler1);
+
+  // Assign messaget:
+  messaget msg2;
+  msg2=msg1;
+
+  // Change its handler:
+  msg2.set_message_handler(handler2);
+
+  msg2.status() << "Test" << messaget::eom;
+
+  CHECK(sstream1.str()=="");
+  CHECK(sstream2.str()=="Test\n");
+}