Merge pull request #2210 from tautschnig/verbosity-cleanup

Verbosity parsing/handling cleanup

Author: tautschnig

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