Merge pull request #5593 from tautschnig/messaget-string_instrumentationt

string_instrumentationt isn't messaget

Author: tautschnig

src/cbmc/cbmc_parse_options.cpp

@@ -894,7 +894,7 @@ bool cbmc_parse_optionst::process_goto_program(
   add_malloc_may_fail_variable_initializations(goto_model);
 
   if(options.get_bool_option("string-abstraction"))
-    string_instrumentation(goto_model, log.get_message_handler());
+    string_instrumentation(goto_model);
 
   // remove function pointers
   log.status() << "Removal of function pointers and virtual functions"

src/goto-programs/string_instrumentation.cpp

@@ -17,7 +17,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/c_types.h>
 #include <util/config.h>
 #include <util/invariant.h>
-#include <util/message.h>
 #include <util/std_code.h>
 #include <util/std_expr.h>
 #include <util/string_constant.h>
@@ -52,15 +51,11 @@ exprt buffer_size(const exprt &what)
   return result;
 }
 
-class string_instrumentationt:public messaget
+class string_instrumentationt
 {
 public:
-  string_instrumentationt(
-    symbol_tablet &_symbol_table,
-    message_handlert &_message_handler):
-    messaget(_message_handler),
-    symbol_table(_symbol_table),
-    ns(_symbol_table)
+  explicit string_instrumentationt(symbol_tablet &_symbol_table)
+    : symbol_table(_symbol_table), ns(_symbol_table)
   {
   }
 
@@ -156,29 +151,24 @@ class string_instrumentationt:public messaget
 
 void string_instrumentation(
   symbol_tablet &symbol_table,
-  message_handlert &message_handler,
   goto_programt &dest)
 {
-  string_instrumentationt string_instrumentation(symbol_table, message_handler);
+  string_instrumentationt string_instrumentation{symbol_table};
   string_instrumentation(dest);
 }
 
 void string_instrumentation(
   symbol_tablet &symbol_table,
-  message_handlert &message_handler,
   goto_functionst &dest)
 {
-  string_instrumentationt string_instrumentation(symbol_table, message_handler);
+  string_instrumentationt string_instrumentation{symbol_table};
   string_instrumentation(dest);
 }
 
-void string_instrumentation(
-  goto_modelt &goto_model,
-  message_handlert &message_handler)
+void string_instrumentation(goto_modelt &goto_model)
 {
   string_instrumentation(
     goto_model.symbol_table,
-    message_handler,
     goto_model.goto_functions);
 }
 

src/goto-programs/string_instrumentation.h

@@ -16,7 +16,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/exception_utils.h>
 
-class message_handlert;
 class goto_modelt;
 
 class incorrect_source_program_exceptiont : public cprover_exception_baset
@@ -40,17 +39,13 @@ class incorrect_source_program_exceptiont : public cprover_exception_baset
 
 void string_instrumentation(
   symbol_tablet &,
-  message_handlert &,
   goto_programt &);
 
 void string_instrumentation(
   symbol_tablet &,
-  message_handlert &,
   goto_functionst &);
 
-void string_instrumentation(
-  goto_modelt &,
-  message_handlert &);
+void string_instrumentation(goto_modelt &);
 
 predicate_exprt is_zero_string(const exprt &what, bool write = false);
 exprt zero_string_length(const exprt &what, bool write=false);