fixup! Stop propt inheriting from messaget

Author: romainbrenguier

src/cbmc/cbmc_solvers.cpp

@@ -74,7 +74,7 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_default()
     solver->set_prop(util_make_unique<satcheckt>());
   }
 
-  solver->prop().message.set_message_handler(message_handler);
+  solver->prop().set_message_handler(message_handler);
 
   auto bv_pointers = util_make_unique<bv_pointerst>(ns, solver->prop());
 
@@ -94,7 +94,7 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_dimacs()
   no_incremental_check();
 
   auto prop=util_make_unique<dimacs_cnft>();
-  prop->message.set_message_handler(message_handler);
+  prop->set_message_handler(message_handler);
 
   std::string filename=options.get_option("outfile");
 
@@ -115,7 +115,7 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_bv_refinement()
     return util_make_unique<satcheck_no_simplifiert>();
   }();
 
-  prop->message.set_message_handler(message_handler);
+  prop->set_message_handler(message_handler);
 
   bv_refinementt::infot info;
   info.ns=&ns;
@@ -143,7 +143,7 @@ std::unique_ptr<cbmc_solverst::solvert> cbmc_solverst::get_string_refinement()
   string_refinementt::infot info;
   info.ns=&ns;
   auto prop=util_make_unique<satcheck_no_simplifiert>();
-  prop->message.set_message_handler(message_handler);
+  prop->set_message_handler(message_handler);
   info.prop=prop.get();
   info.refinement_bound=DEFAULT_MAX_NB_REFINEMENT;
   info.output_xml = output_xml_in_refinement;

src/solvers/flattening/arrays.cpp

@@ -48,7 +48,7 @@ literalt arrayst::record_array_equality(
   // check types
   if(!base_type_eq(op0.type(), op1.type(), ns))
   {
-    prop.message.error() << equality.pretty() << messaget::eom;
+    error() << equality.pretty() << messaget::eom;
     DATA_INVARIANT(
       false,
       "record_array_equality got equality without matching types");
@@ -117,7 +117,7 @@ void arrayst::collect_arrays(const exprt &a)
     // check types
     if(!base_type_eq(array_type, with_expr.old().type(), ns))
     {
-      prop.message.error() << a.pretty() << messaget::eom;
+      error() << a.pretty() << messaget::eom;
       DATA_INVARIANT(false, "collect_arrays got 'with' without matching types");
     }
 
@@ -135,7 +135,7 @@ void arrayst::collect_arrays(const exprt &a)
     // check types
     if(!base_type_eq(array_type, update_expr.old().type(), ns))
     {
-      prop.message.error() << a.pretty() << messaget::eom;
+      error() << a.pretty() << messaget::eom;
       DATA_INVARIANT(
         false,
         "collect_arrays got 'update' without matching types");
@@ -157,14 +157,14 @@ void arrayst::collect_arrays(const exprt &a)
     // check types
     if(!base_type_eq(array_type, if_expr.true_case().type(), ns))
     {
-      prop.message.error() << a.pretty() << messaget::eom;
+      error() << a.pretty() << messaget::eom;
       DATA_INVARIANT(false, "collect_arrays got if without matching types");
     }
 
     // check types
     if(!base_type_eq(array_type, if_expr.false_case().type(), ns))
     {
-      prop.message.error() << a.pretty() << messaget::eom;
+      error() << a.pretty() << messaget::eom;
       DATA_INVARIANT(false, "collect_arrays got if without matching types");
     }
 
@@ -518,7 +518,7 @@ void arrayst::add_array_constraints_with(
 
     if(index_expr.type()!=value.type())
     {
-      prop.message.error() << expr.pretty() << messaget::eom;
+      error() << expr.pretty() << messaget::eom;
       DATA_INVARIANT(
         false,
         "with-expression operand should match array element type");

src/solvers/prop/prop.h

@@ -24,8 +24,8 @@ Author: Daniel Kroening, [email protected]
 class propt
 {
 public:
-  messaget message;
   propt() { }
+
   virtual ~propt() { }
 
   // boolean operators
@@ -117,9 +117,16 @@ class propt
     message.warning() << "CPU limit ignored (not implemented)" << messaget::eom;
   }
 
+  void set_message_handler(message_handlert &message_handler)
+  {
+    message.set_message_handler(message_handler);
+  }
+
 protected:
   // to avoid a temporary for lcnf(...)
   bvt lcnf_bv;
+
+  messaget message;
 };
 
 #endif // CPROVER_SOLVERS_PROP_PROP_H

src/solvers/smt2/smt2_solver.cpp

@@ -229,7 +229,7 @@ int solver(std::istream &in)
 
   satcheckt satcheck;
   boolbvt boolbv(ns, satcheck);
-  satcheck.message.set_message_handler(message_handler);
+  satcheck.set_message_handler(message_handler);
   boolbv.set_message_handler(message_handler);
 
   smt2_solvert smt2_solver(in, boolbv);