Removed legacy messaget interface, removed message_clientt

tautschnig · tautschnig · commit 9b79eb6ba694 · 2017-04-04T18:18:07.000+01:00
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
@@ -661,7 +661,7 @@ int cbmc_parse_optionst::get_goto_program(
 
       language->set_message_handler(get_message_handler());
 
-      status("Parsing", filename);
+      status() << "Parsing " << filename << eom;
 
       if(language->parse(infile, filename))
       {
diff --git a/src/clobber/clobber_parse_options.cpp b/src/clobber/clobber_parse_options.cpp
@@ -326,7 +326,7 @@ bool clobber_parse_optionst::get_goto_program(
 
       language->set_message_handler(get_message_handler());
 
-      status("Parsing", filename);
+      status() << "Parsing " << filename << eom;
 
       if(language->parse(infile, filename))
       {
diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp
@@ -383,7 +383,7 @@ Function: compilet::link
 bool compilet::link()
 {
   // "compile" hitherto uncompiled functions
-  print(8, "Compiling functions");
+  statistics() << "Compiling functions" << eom;
   convert_symbols(compiled_functions);
 
   // parse object files
@@ -554,7 +554,7 @@ bool compilet::parse(const std::string &file_name)
 
   if(mode==PREPROCESS_ONLY)
   {
-    print(8, "Preprocessing: "+file_name);
+    statistics() << "Preprocessing: " << file_name << eom;
 
     std::ostream *os = &std::cout;
     std::ofstream ofs;
@@ -576,7 +576,7 @@ bool compilet::parse(const std::string &file_name)
   }
   else
   {
-    print(8, "Parsing: "+file_name);
+    statistics() << "Parsing: " << file_name << eom;
 
     if(language.parse(infile, file_name))
     {
@@ -608,7 +608,7 @@ bool compilet::parse_stdin()
 
   language.set_message_handler(get_message_handler());
 
-  print(8, "Parsing: (stdin)");
+  statistics() << "Parsing: (stdin)" << eom;
 
   if(mode==PREPROCESS_ONLY)
   {
@@ -872,7 +872,7 @@ void compilet::convert_symbols(goto_functionst &dest)
           s_it->second.value.id()!="compiled" &&
           s_it->second.value.is_not_nil())
       {
-        print(9, "Compiling "+id2string(s_it->first));
+        debug() << "Compiling " << s_it->first << eom;
         converter.convert_function(s_it->first);
         s_it->second.value=exprt("compiled");
       }
diff --git a/src/goto-programs/get_goto_model.cpp b/src/goto-programs/get_goto_model.cpp
@@ -87,7 +87,10 @@ bool get_goto_modelt::operator()(const cmdlinet &_cmdline)
 
         if(lf.language==NULL)
         {
-          error("failed to figure out type of file", filename);
+          source_locationt location;
+          location.set_file(filename);
+          error().source_location=location;
+          error() << "failed to figure out type of file" << eom;
           return true;
         }
 
diff --git a/src/goto-symex/memory_model_pso.cpp b/src/goto-symex/memory_model_pso.cpp
@@ -22,7 +22,7 @@ Function: memory_model_psot::operator()
 
 void memory_model_psot::operator()(symex_target_equationt &equation)
 {
-  print(8, "Adding PSO constraints");
+  statistics() << "Adding PSO constraints" << eom;
 
   build_event_lists(equation);
   build_clock_type(equation);
diff --git a/src/goto-symex/memory_model_sc.cpp b/src/goto-symex/memory_model_sc.cpp
@@ -24,7 +24,7 @@ Function: memory_model_sct::operator()
 
 void memory_model_sct::operator()(symex_target_equationt &equation)
 {
-  print(8, "Adding SC constraints");
+  statistics() << "Adding SC constraints" << eom;
 
   build_event_lists(equation);
   build_clock_type(equation);
diff --git a/src/goto-symex/memory_model_tso.cpp b/src/goto-symex/memory_model_tso.cpp
@@ -25,7 +25,7 @@ Function: memory_model_tsot::operator()
 
 void memory_model_tsot::operator()(symex_target_equationt &equation)
 {
-  print(8, "Adding TSO constraints");
+  statistics() << "Adding TSO constraints" << eom;
 
   build_event_lists(equation);
   build_clock_type(equation);
diff --git a/src/langapi/language_ui.cpp b/src/langapi/language_ui.cpp
@@ -115,7 +115,10 @@ bool language_uit::parse(const std::string &filename)
 
   if(lf.language==NULL)
   {
-    error("failed to figure out type of file", filename);
+    source_locationt location;
+    location.set_file(filename);
+    error().source_location=location;
+    error() << "failed to figure out type of file" << eom;
     return true;
   }
 
diff --git a/src/solvers/prop/prop_conv.cpp b/src/solvers/prop/prop_conv.cpp
@@ -624,9 +624,7 @@ void prop_conv_solvert::ignoring(const exprt &expr)
 {
   // fall through
 
-  std::string msg="warning: ignoring "+expr.pretty();
-
-  print(2, msg);
+  warning() << "warning: ignoring " << expr.pretty() << eom;
 }
 
 /*******************************************************************\
@@ -662,12 +660,12 @@ decision_proceduret::resultt prop_conv_solvert::dec_solve()
   // post-processing isn't incremental yet
   if(!post_processing_done)
   {
-    print(8, "Post-processing");
+    statistics() << "Post-processing" << eom;
     post_process();
     post_processing_done=true;
   }
 
-  print(7, "Solving with "+prop.solver_text());
+  statistics() << "Solving with " << prop.solver_text() << eom;
 
   propt::resultt result=prop.prop_solve();
 
diff --git a/src/solvers/sat/pbs_dimacs_cnf.cpp b/src/solvers/sat/pbs_dimacs_cnf.cpp
@@ -190,7 +190,8 @@ bool pbs_dimacs_cnft::pbs_solve()
           // print(line);
           if(strstr(line.c_str(), "time out")!=NULL)
             {
-              print(6, "WARNING:  TIMED OUT.  SOLUTION MAY BE INCORRECT.\n");
+              status() << "WARNING:  TIMED OUT.  SOLUTION MAY BE INCORRECT."
+                       << eom;
               return satisfied;
             }
           sscanf(line.c_str(), "%*s %*s %*s %d", &opt_sum);
diff --git a/src/util/cout_message.cpp b/src/util/cout_message.cpp
@@ -190,9 +190,9 @@ void gcc_message_handlert::print(
     else
       dest+=id2string(column)+": ";
 
-    if(level==message_clientt::M_ERROR)
+    if(level==messaget::M_ERROR)
       dest+="error: ";
-    else if(level==message_clientt::M_WARNING)
+    else if(level==messaget::M_WARNING)
       dest+="warning: ";
   }
 
diff --git a/src/util/message.cpp b/src/util/message.cpp
@@ -88,7 +88,7 @@ void message_handlert::print(
 
 /*******************************************************************\
 
-Function: messaget::print
+Function: messaget::~messaget
 
   Inputs:
 
@@ -98,65 +98,6 @@ Function: messaget::print
 
 \*******************************************************************/
 
-void messaget::print(unsigned level, const std::string &message)
+messaget::~messaget()
 {
-  if(message_handler!=NULL)
-    message_handler->print(level, message);
-}
-
-/*******************************************************************\
-
-Function: messaget::print
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-void messaget::print(
-  unsigned level,
-  const std::string &message,
-  int sequence_number,
-  const source_locationt &location)
-{
-  if(message_handler!=NULL)
-    message_handler->print(level, message, sequence_number,
-                           location);
-}
-
-/*******************************************************************\
-
-Function: message_clientt::~message_clientt
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-message_clientt::~message_clientt()
-{
-}
-
-/*******************************************************************\
-
-Function: message_clientt::set_message_handler
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-void message_clientt::set_message_handler(
-  message_handlert &_message_handler)
-{
-  message_handler=&_message_handler;
 }
diff --git a/src/util/message.h b/src/util/message.h
diff --git a/src/util/parser.cpp b/src/util/parser.cpp

Original file line number	Diff line number	Diff line change
`@@ -661,7 +661,7 @@ int cbmc_parse_optionst::get_goto_program(`
`661`	`661`
`662`	`662`	`language->set_message_handler(get_message_handler());`
`663`	`663`
`664`		`- status("Parsing", filename);`
	`664`	`+ status() << "Parsing " << filename << eom;`
`665`	`665`
`666`	`666`	`if(language->parse(infile, filename))`
`667`	`667`	`{`
Original file line number	Diff line number	Diff line change
`@@ -326,7 +326,7 @@ bool clobber_parse_optionst::get_goto_program(`
`326`	`326`
`327`	`327`	`language->set_message_handler(get_message_handler());`
`328`	`328`
`329`		`- status("Parsing", filename);`
	`329`	`+ status() << "Parsing " << filename << eom;`
`330`	`330`
`331`	`331`	`if(language->parse(infile, filename))`
`332`	`332`	`{`
Original file line number	Diff line number	Diff line change
`@@ -383,7 +383,7 @@ Function: compilet::link`
`383`	`383`	`bool compilet::link()`
`384`	`384`	`{`
`385`	`385`	`// "compile" hitherto uncompiled functions`
`386`		`- print(8, "Compiling functions");`
	`386`	`+ statistics() << "Compiling functions" << eom;`
`387`	`387`	`convert_symbols(compiled_functions);`
`388`	`388`
`389`	`389`	`// parse object files`
`@@ -554,7 +554,7 @@ bool compilet::parse(const std::string &file_name)`
`554`	`554`
`555`	`555`	`if(mode==PREPROCESS_ONLY)`
`556`	`556`	`{`
`557`		`- print(8, "Preprocessing: "+file_name);`
	`557`	`+ statistics() << "Preprocessing: " << file_name << eom;`
`558`	`558`
`559`	`559`	`std::ostream *os = &std::cout;`
`560`	`560`	`std::ofstream ofs;`
`@@ -576,7 +576,7 @@ bool compilet::parse(const std::string &file_name)`
`576`	`576`	`}`
`577`	`577`	`else`
`578`	`578`	`{`
`579`		`- print(8, "Parsing: "+file_name);`
	`579`	`+ statistics() << "Parsing: " << file_name << eom;`
`580`	`580`
`581`	`581`	`if(language.parse(infile, file_name))`
`582`	`582`	`{`
`@@ -608,7 +608,7 @@ bool compilet::parse_stdin()`
`608`	`608`
`609`	`609`	`language.set_message_handler(get_message_handler());`
`610`	`610`
`611`		`- print(8, "Parsing: (stdin)");`
	`611`	`+ statistics() << "Parsing: (stdin)" << eom;`
`612`	`612`
`613`	`613`	`if(mode==PREPROCESS_ONLY)`
`614`	`614`	`{`
`@@ -872,7 +872,7 @@ void compilet::convert_symbols(goto_functionst &dest)`
`872`	`872`	`s_it->second.value.id()!="compiled" &&`
`873`	`873`	`s_it->second.value.is_not_nil())`
`874`	`874`	`{`
`875`		`- print(9, "Compiling "+id2string(s_it->first));`
	`875`	`+ debug() << "Compiling " << s_it->first << eom;`
`876`	`876`	`converter.convert_function(s_it->first);`
`877`	`877`	`s_it->second.value=exprt("compiled");`
`878`	`878`	`}`
Original file line number	Diff line number	Diff line change
`@@ -87,7 +87,10 @@ bool get_goto_modelt::operator()(const cmdlinet &_cmdline)`
`87`	`87`
`88`	`88`	`if(lf.language==NULL)`
`89`	`89`	`{`
`90`		`- error("failed to figure out type of file", filename);`
	`90`	`+ source_locationt location;`
	`91`	`+ location.set_file(filename);`
	`92`	`+ error().source_location=location;`
	`93`	`+ error() << "failed to figure out type of file" << eom;`
`91`	`94`	`return true;`
`92`	`95`	`}`
`93`	`96`
Original file line number	Diff line number	Diff line change
`@@ -22,7 +22,7 @@ Function: memory_model_psot::operator()`
`22`	`22`
`23`	`23`	`void memory_model_psot::operator()(symex_target_equationt &equation)`
`24`	`24`	`{`
`25`		`- print(8, "Adding PSO constraints");`
	`25`	`+ statistics() << "Adding PSO constraints" << eom;`
`26`	`26`
`27`	`27`	`build_event_lists(equation);`
`28`	`28`	`build_clock_type(equation);`
Original file line number	Diff line number	Diff line change
`@@ -24,7 +24,7 @@ Function: memory_model_sct::operator()`
`24`	`24`
`25`	`25`	`void memory_model_sct::operator()(symex_target_equationt &equation)`
`26`	`26`	`{`
`27`		`- print(8, "Adding SC constraints");`
	`27`	`+ statistics() << "Adding SC constraints" << eom;`
`28`	`28`
`29`	`29`	`build_event_lists(equation);`
`30`	`30`	`build_clock_type(equation);`
Original file line number	Diff line number	Diff line change
`@@ -25,7 +25,7 @@ Function: memory_model_tsot::operator()`
`25`	`25`
`26`	`26`	`void memory_model_tsot::operator()(symex_target_equationt &equation)`
`27`	`27`	`{`
`28`		`- print(8, "Adding TSO constraints");`
	`28`	`+ statistics() << "Adding TSO constraints" << eom;`
`29`	`29`
`30`	`30`	`build_event_lists(equation);`
`31`	`31`	`build_clock_type(equation);`
Original file line number	Diff line number	Diff line change
`@@ -115,7 +115,10 @@ bool language_uit::parse(const std::string &filename)`
`115`	`115`
`116`	`116`	`if(lf.language==NULL)`
`117`	`117`	`{`
`118`		`- error("failed to figure out type of file", filename);`
	`118`	`+ source_locationt location;`
	`119`	`+ location.set_file(filename);`
	`120`	`+ error().source_location=location;`
	`121`	`+ error() << "failed to figure out type of file" << eom;`
`119`	`122`	`return true;`
`120`	`123`	`}`
`121`	`124`
Original file line number	Diff line number	Diff line change
`@@ -624,9 +624,7 @@ void prop_conv_solvert::ignoring(const exprt &expr)`
`624`	`624`	`{`
`625`	`625`	`// fall through`
`626`	`626`
`627`		`- std::string msg="warning: ignoring "+expr.pretty();`
`628`		`-`
`629`		`- print(2, msg);`
	`627`	`+ warning() << "warning: ignoring " << expr.pretty() << eom;`
`630`	`628`	`}`
`631`	`629`
`632`	`630`	`/*******************************************************************\`
`@@ -662,12 +660,12 @@ decision_proceduret::resultt prop_conv_solvert::dec_solve()`
`662`	`660`	`// post-processing isn't incremental yet`
`663`	`661`	`if(!post_processing_done)`
`664`	`662`	`{`
`665`		`- print(8, "Post-processing");`
	`663`	`+ statistics() << "Post-processing" << eom;`
`666`	`664`	`post_process();`
`667`	`665`	`post_processing_done=true;`
`668`	`666`	`}`
`669`	`667`
`670`		`- print(7, "Solving with "+prop.solver_text());`
	`668`	`+ statistics() << "Solving with " << prop.solver_text() << eom;`
`671`	`669`
`672`	`670`	`propt::resultt result=prop.prop_solve();`
`673`	`671`
Original file line number	Diff line number	Diff line change
`@@ -190,7 +190,8 @@ bool pbs_dimacs_cnft::pbs_solve()`
`190`	`190`	`// print(line);`
`191`	`191`	`if(strstr(line.c_str(), "time out")!=NULL)`
`192`	`192`	`{`
`193`		`- print(6, "WARNING: TIMED OUT. SOLUTION MAY BE INCORRECT.\n");`
	`193`	`+ status() << "WARNING: TIMED OUT. SOLUTION MAY BE INCORRECT."`
	`194`	`+ << eom;`
`194`	`195`	`return satisfied;`
`195`	`196`	`}`
`196`	`197`	`sscanf(line.c_str(), "%s %s %*s %d", &opt_sum);`