Verbosity parsing/handling cleanup

jbmc/src/janalyzer/janalyzer_parse_options.cpp

@@ -51,7 +51,6 @@ Author: Daniel Kroening, [email protected]
 #include <util/config.h>
 #include <util/exit_codes.h>
 #include <util/options.h>
-#include <util/string2int.h>
 #include <util/unicode.h>
 
 #include <cbmc/version.h>
@@ -74,21 +73,6 @@ void janalyzer_parse_optionst::register_languages()
   register_language(new_java_bytecode_language);
 }
 
-void janalyzer_parse_optionst::eval_verbosity()
-{
-  // this is our default verbosity
-  unsigned int v = messaget::M_STATISTICS;
-
-  if(cmdline.isset("verbosity"))
-  {
-    v = unsafe_string2unsigned(cmdline.get_value("verbosity"));
-    if(v > 10)
-      v = 10;
-  }
-
-  ui_message_handler.set_verbosity(v);
-}
-
 void janalyzer_parse_optionst::get_command_line_options(optionst &options)
 {
   if(config.set(cmdline))
@@ -356,7 +340,8 @@ int janalyzer_parse_optionst::doit()
 
   optionst options;
   get_command_line_options(options);
-  eval_verbosity();
+  eval_verbosity(
+    cmdline.get_value("verbosity"), messaget::M_STATISTICS, ui_message_handler);
 
   //
   // Print a banner

jbmc/src/janalyzer/janalyzer_parse_options.h

@@ -173,8 +173,6 @@ class janalyzer_parse_optionst : public parse_options_baset, public messaget
 
   ai_baset *build_analyzer(const optionst &, const namespacet &ns);
 
-  void eval_verbosity();
-
   ui_message_handlert::uit get_ui()
   {
     return ui_message_handler.get_ui();

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -17,7 +17,6 @@ Author: Daniel Kroening, [email protected]
 #include <memory>
 
 #include <util/exit_codes.h>
-#include <util/string2int.h>
 #include <util/config.h>
 #include <util/unicode.h>
 #include <util/invariant.h>
@@ -82,21 +81,6 @@ ::jbmc_parse_optionst::jbmc_parse_optionst(
 {
 }
 
-void jbmc_parse_optionst::eval_verbosity()
-{
-  // this is our default verbosity
-  unsigned int v=messaget::M_STATISTICS;
-
-  if(cmdline.isset("verbosity"))
-  {
-    v=unsafe_string2unsigned(cmdline.get_value("verbosity"));
-    if(v>10)
-      v=10;
-  }
-
-  ui_message_handler.set_verbosity(v);
-}
-
 void jbmc_parse_optionst::get_command_line_options(optionst &options)
 {
   if(config.set(cmdline))
@@ -443,7 +427,8 @@ int jbmc_parse_optionst::doit()
     return 6; // should contemplate EX_SOFTWARE from sysexits.h
   }
 
-  eval_verbosity();
+  eval_verbosity(
+    cmdline.get_value("verbosity"), messaget::M_STATISTICS, ui_message_handler);
 
   //
   // Print a banner

jbmc/src/jbmc/jbmc_parse_options.h

@@ -117,7 +117,6 @@ class jbmc_parse_optionst:
   object_factory_parameterst object_factory_params;
   bool stub_objects_are_not_null;
 
-  void eval_verbosity();
   void get_command_line_options(optionst &);
   int get_goto_program(
     std::unique_ptr<goto_modelt> &goto_model, const optionst &);

jbmc/src/jdiff/jdiff_parse_options.cpp

@@ -20,7 +20,6 @@ Author: Peter Schrammel
 #include <util/exit_codes.h>
 #include <util/make_unique.h>
 #include <util/options.h>
-#include <util/string2int.h>
 
 #include <langapi/language.h>
 
@@ -82,21 +81,6 @@ ::jdiff_parse_optionst::jdiff_parse_optionst(
 {
 }
 
-void jdiff_parse_optionst::eval_verbosity()
-{
-  // this is our default verbosity
-  unsigned int v = messaget::M_STATISTICS;
-
-  if(cmdline.isset("verbosity"))
-  {
-    v = unsafe_string2unsigned(cmdline.get_value("verbosity"));
-    if(v > 10)
-      v = 10;
-  }
-
-  ui_message_handler.set_verbosity(v);
-}
-
 void jdiff_parse_optionst::get_command_line_options(optionst &options)
 {
   if(config.set(cmdline))
@@ -211,7 +195,8 @@ int jdiff_parse_optionst::doit()
 
   optionst options;
   get_command_line_options(options);
-  eval_verbosity();
+  eval_verbosity(
+    cmdline.get_value("verbosity"), messaget::M_STATISTICS, ui_message_handler);
 
   //
   // Print a banner

jbmc/src/jdiff/jdiff_parse_options.h

@@ -66,8 +66,6 @@ class jdiff_parse_optionst : public parse_options_baset, public jdiff_languagest
   virtual bool
   process_goto_program(const optionst &options, goto_modelt &goto_model);
 
-  void eval_verbosity();
-
   void preprocessing();
 };
 

src/cbmc/cbmc_parse_options.cpp

@@ -16,7 +16,6 @@ Author: Daniel Kroening, [email protected]
 #include <iostream>
 #include <memory>
 
-#include <util/string2int.h>
 #include <util/config.h>
 #include <util/unicode.h>
 #include <util/invariant.h>
@@ -100,21 +99,6 @@ void cbmc_parse_optionst::set_default_options(optionst &options)
   options.set_option("arrays-uf", "auto");
 }
 
-void cbmc_parse_optionst::eval_verbosity()
-{
-  // this is our default verbosity
-  unsigned int v=messaget::M_STATISTICS;
-
-  if(cmdline.isset("verbosity"))
-  {
-    v=unsafe_string2unsigned(cmdline.get_value("verbosity"));
-    if(v>10)
-      v=10;
-  }
-
-  ui_message_handler.set_verbosity(v);
-}
-
 void cbmc_parse_optionst::get_command_line_options(optionst &options)
 {
   if(config.set(cmdline))
@@ -435,7 +419,8 @@ int cbmc_parse_optionst::doit()
     return CPROVER_EXIT_EXCEPTION;
   }
 
-  eval_verbosity();
+  eval_verbosity(
+    cmdline.get_value("verbosity"), messaget::M_STATISTICS, ui_message_handler);
 
   //
   // Print a banner

src/cbmc/cbmc_parse_options.h

@@ -112,7 +112,6 @@ class cbmc_parse_optionst:
   ui_message_handlert ui_message_handler;
   const path_strategy_choosert path_strategy_chooser;
 
-  void eval_verbosity();
   void register_languages();
   void get_command_line_options(optionst &);
   void preprocessing();

src/clobber/clobber_parse_options.cpp

@@ -15,7 +15,6 @@ Author: Daniel Kroening, [email protected]
 #include <fstream>
 #include <cstdlib>
 
-#include <util/string2int.h>
 #include <util/config.h>
 #include <util/options.h>
 #include <util/memory_info.h>
@@ -45,23 +44,6 @@ clobber_parse_optionst::clobber_parse_optionst(int argc, const char **argv):
 {
 }
 
-void clobber_parse_optionst::eval_verbosity()
-{
-  // this is our default verbosity
-  int v=messaget::M_STATISTICS;
-
-  if(cmdline.isset("verbosity"))
-  {
-    v=unsafe_string2int(cmdline.get_value("verbosity"));
-    if(v<0)
-      v=0;
-    else if(v>10)
-      v=10;
-  }
-
-  ui_message_handler.set_verbosity(v);
-}
-
 void clobber_parse_optionst::get_command_line_options(optionst &options)
 {
   if(config.set(cmdline))
@@ -115,7 +97,8 @@ int clobber_parse_optionst::doit()
   optionst options;
   get_command_line_options(options);
 
-  eval_verbosity();
+  eval_verbosity(
+    cmdline.get_value("verbosity"), messaget::M_STATISTICS, ui_message_handler);
 
   goto_modelt goto_model;
 

src/clobber/clobber_parse_options.h

@@ -66,8 +66,6 @@ class clobber_parse_optionst:
   void report_success();
   void report_failure();
   void show_counterexample(const class goto_tracet &);
-
-  void eval_verbosity();
 };
 
 #endif // CPROVER_CLOBBER_CLOBBER_PARSE_OPTIONS_H

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -47,7 +47,6 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/options.h>
 #include <util/config.h>
-#include <util/string2int.h>
 #include <util/unicode.h>
 #include <util/exit_codes.h>
 
@@ -76,21 +75,6 @@ void goto_analyzer_parse_optionst::register_languages()
   register_language(new_jsil_language);
 }
 
-void goto_analyzer_parse_optionst::eval_verbosity()
-{
-  // this is our default verbosity
-  unsigned int v=messaget::M_STATISTICS;
-
-  if(cmdline.isset("verbosity"))
-  {
-    v=unsafe_string2unsigned(cmdline.get_value("verbosity"));
-    if(v>10)
-      v=10;
-  }
-
-  ui_message_handler.set_verbosity(v);
-}
-
 void goto_analyzer_parse_optionst::get_command_line_options(optionst &options)
 {
   if(config.set(cmdline))
@@ -381,7 +365,8 @@ int goto_analyzer_parse_optionst::doit()
 
   optionst options;
   get_command_line_options(options);
-  eval_verbosity();
+  eval_verbosity(
+    cmdline.get_value("verbosity"), messaget::M_STATISTICS, ui_message_handler);
 
   //
   // Print a banner

src/goto-analyzer/goto_analyzer_parse_options.h

@@ -175,8 +175,6 @@ class goto_analyzer_parse_optionst:
 
   ai_baset *build_analyzer(const optionst &, const namespacet &ns);
 
-  void eval_verbosity();
-
   ui_message_handlert::uit get_ui()
   {
     return ui_message_handler.get_ui();

src/goto-cc/armcc_mode.cpp

@@ -21,7 +21,6 @@ Author: CM Wintersteiger, 2006
 
 #include <iostream>
 
-#include <util/string2int.h>
 #include <util/message.h>
 #include <util/prefix.h>
 #include <util/config.h>
@@ -37,8 +36,6 @@ int armcc_modet::doit()
     return EX_OK;
   }
 
-  unsigned int verbosity=1;
-
   compilet compiler(cmdline, message_handler, cmdline.isset("diag_error="));
 
   #if 0
@@ -49,11 +46,8 @@ int armcc_modet::doit()
     has_prefix(base_name, "goto-link");
   #endif
 
-  if(cmdline.isset("verbosity"))
-    verbosity=unsafe_string2int(cmdline.get_value("verbosity"));
-
-  compiler.set_message_handler(get_message_handler());
-  message_handler.set_verbosity(verbosity);
+  const auto verbosity = eval_verbosity(
+    cmdline.get_value("verbosity"), messaget::M_ERROR, message_handler);
 
   debug() << "ARM mode" << eom;
 
@@ -136,7 +130,7 @@ int armcc_modet::doit()
     compiler.output_file_executable="a.out";
   }
 
-  if(verbosity>8)
+  if(verbosity > messaget::M_STATISTICS)
   {
     std::list<std::string>::iterator it;
 

src/goto-cc/as_mode.cpp

@@ -24,7 +24,6 @@ Author: Michael Tautschnig
 #include <cstring>
 
 #include <util/run.h>
-#include <util/string2int.h>
 #include <util/tempdir.h>
 #include <util/config.h>
 #include <util/get_base_name.h>
@@ -76,8 +75,6 @@ int as_modet::doit()
     return EX_OK;
   }
 
-  unsigned int verbosity=1;
-
   bool act_as_as86=
     base_name=="as86" ||
     base_name.find("goto-as86")!=std::string::npos;
@@ -101,13 +98,10 @@ int as_modet::doit()
     return EX_OK; // Exit!
   }
 
-  if(cmdline.isset("w-") || cmdline.isset("warn"))
-    verbosity=2;
-
-  if(cmdline.isset("verbosity"))
-    verbosity=unsafe_string2unsigned(cmdline.get_value("verbosity"));
-
-  message_handler.set_verbosity(verbosity);
+  auto default_verbosity = (cmdline.isset("w-") || cmdline.isset("warn")) ?
+    messaget::M_WARNING : messaget::M_ERROR;
+  eval_verbosity(
+    cmdline.get_value("verbosity"), default_verbosity, message_handler);
 
   if(act_as_as86)
   {