Merge pull request #5620 from tautschnig/messaget-string_abstraction

string_abstractiont isn't a messaget

Author: tautschnig

src/goto-programs/string_abstraction.cpp

@@ -17,6 +17,7 @@ Author: Daniel Kroening, [email protected]
 #include <util/c_types.h>
 #include <util/exception_utils.h>
 #include <util/expr_util.h>
+#include <util/message.h>
 #include <util/pointer_predicates.h>
 #include <util/string_constant.h>
 
@@ -44,8 +45,9 @@ bool string_abstractiont::build_wrap(
     !(dest.type().id() == ID_array && a_t.id() == ID_pointer &&
       dest.type().subtype() == a_t.subtype()))
   {
-    warning() << "warning: inconsistent abstract type for "
-              << object.pretty() << eom;
+    messaget log{message_handler};
+    log.warning() << "warning: inconsistent abstract type for "
+                  << object.pretty() << messaget::eom;
     return true;
   }
 
@@ -92,13 +94,13 @@ void string_abstraction(
 
 string_abstractiont::string_abstractiont(
   symbol_tablet &_symbol_table,
-  message_handlert &_message_handler):
-  messaget(_message_handler),
-  arg_suffix("#strarg"),
-  sym_suffix("#str$fcn"),
-  symbol_table(_symbol_table),
-  ns(_symbol_table),
-  temporary_counter(0)
+  message_handlert &_message_handler)
+  : arg_suffix("#strarg"),
+    sym_suffix("#str$fcn"),
+    symbol_table(_symbol_table),
+    ns(_symbol_table),
+    temporary_counter(0),
+    message_handler(_message_handler)
 {
   struct_typet s({{"is_zero", build_type(whatt::IS_ZERO)},
                   {"length", build_type(whatt::LENGTH)},

src/goto-programs/string_abstraction.h

@@ -13,18 +13,19 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_GOTO_PROGRAMS_STRING_ABSTRACTION_H
 
 #include <util/symbol_table.h>
-#include <util/message.h>
 #include <util/config.h>
 #include <util/std_expr.h>
 
 #include "goto_model.h"
 
+class message_handlert;
+
 /// Replace all uses of `char *` by a struct that carries that string, and also
 /// the underlying allocation and the C string length.
 /// This will become useful (with some modifications) for supporting strings in
 /// the C frontend, as the string solver expects a struct that bundles the
 /// string length and the underlying character array.
-class string_abstractiont:public messaget
+class string_abstractiont
 {
 public:
   string_abstractiont(
@@ -40,6 +41,7 @@ class string_abstractiont:public messaget
   symbol_tablet &symbol_table;
   namespacet ns;
   unsigned temporary_counter;
+  message_handlert &message_handler;
 
   typedef ::std::map< typet, typet > abstraction_types_mapt;
   abstraction_types_mapt abstraction_types_map;