Merge pull request #6089 from tautschnig/version-output-refactor

tautschnig · web-flow · commit 247380f02be0 · 2021-05-07T14:28:11.000+02:00
De-duplicate version output code
diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp
@@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "janalyzer_parse_options.h"
 
-#include <climits>
 #include <cstdlib> // exit()
 #include <fstream>
 #include <iostream>
@@ -346,13 +345,7 @@ int janalyzer_parse_optionst::doit()
   messaget::eval_verbosity(
     cmdline.get_value("verbosity"), messaget::M_STATISTICS, ui_message_handler);
 
-  //
-  // Print a banner
-  //
-  log.status() << "JANALYZER version " << CBMC_VERSION << " "
-               << sizeof(void *) * CHAR_BIT << "-bit "
-               << config.this_architecture() << " "
-               << config.this_operating_system() << messaget::eom;
+  log_version_and_architecture("JANALYZER");
 
   register_languages();
 
diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp
@@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "jbmc_parse_options.h"
 
-#include <climits>
 #include <cstdlib> // exit()
 #include <iostream>
 #include <memory>
@@ -478,13 +477,7 @@ int jbmc_parse_optionst::doit()
   optionst options;
   get_command_line_options(options);
 
-  //
-  // Print a banner
-  //
-  log.status() << "JBMC version " << CBMC_VERSION << " "
-               << sizeof(void *) * CHAR_BIT << "-bit "
-               << config.this_architecture() << " "
-               << config.this_operating_system() << messaget::eom;
+  log_version_and_architecture("JBMC");
 
   // output the options
   switch(ui_message_handler.get_ui())
diff --git a/jbmc/src/jdiff/jdiff_parse_options.cpp b/jbmc/src/jdiff/jdiff_parse_options.cpp
@@ -11,7 +11,6 @@ Author: Peter Schrammel
 
 #include "jdiff_parse_options.h"
 
-#include <climits>
 #include <cstdlib> // exit()
 #include <iostream>
 
@@ -175,13 +174,7 @@ int jdiff_parse_optionst::doit()
   messaget::eval_verbosity(
     cmdline.get_value("verbosity"), messaget::M_STATISTICS, ui_message_handler);
 
-  //
-  // Print a banner
-  //
-  log.status() << "JDIFF version " << CBMC_VERSION << " "
-               << sizeof(void *) * CHAR_BIT << "-bit "
-               << config.this_architecture() << " "
-               << config.this_operating_system() << messaget::eom;
+  log_version_and_architecture("JDIFF");
 
   if(cmdline.args.size() != 2)
   {
diff --git a/scripts/expected_doxygen_warnings.txt b/scripts/expected_doxygen_warnings.txt
@@ -2,7 +2,7 @@ warning: Include graph for 'goto_instrument_parse_options.cpp' not generated, to
 warning: Included by graph for 'goto_model.h' not generated, too many nodes (95), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'arith_tools.h' not generated, too many nodes (167), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'c_types.h' not generated, too many nodes (128), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
-warning: Included by graph for 'config.h' not generated, too many nodes (77), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
+warning: Included by graph for 'config.h' not generated, too many nodes (78), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'invariant.h' not generated, too many nodes (172), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'irep.h' not generated, too many nodes (80), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
 warning: Included by graph for 'message.h' not generated, too many nodes (97), threshold is 60. Consider increasing DOT_GRAPH_MAX_NODES.
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
@@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "cbmc_parse_options.h"
 
-#include <climits>
 #include <cstdlib> // exit()
 #include <fstream>
 #include <iostream>
@@ -517,13 +516,7 @@ int cbmc_parse_optionst::doit()
   messaget::eval_verbosity(
     cmdline.get_value("verbosity"), messaget::M_STATISTICS, ui_message_handler);
 
-  //
-  // Print a banner
-  //
-  log.status() << "CBMC version " << CBMC_VERSION << " "
-               << sizeof(void *) * CHAR_BIT << "-bit "
-               << config.this_architecture() << " "
-               << config.this_operating_system() << messaget::eom;
+  log_version_and_architecture("CBMC");
 
   //
   // Unwinding of transition systems is done by hw-cbmc.
diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp
@@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "goto_analyzer_parse_options.h"
 
-#include <climits>
 #include <cstdlib> // exit()
 #include <fstream>
 #include <iostream>
@@ -394,13 +393,7 @@ int goto_analyzer_parse_optionst::doit()
   messaget::eval_verbosity(
     cmdline.get_value("verbosity"), messaget::M_STATISTICS, ui_message_handler);
 
-  //
-  // Print a banner
-  //
-  log.status() << "GOTO-ANALYSER version " << CBMC_VERSION << " "
-               << sizeof(void *) * CHAR_BIT << "-bit "
-               << config.this_architecture() << " "
-               << config.this_operating_system() << messaget::eom;
+  log_version_and_architecture("GOTO-ANALYZER");
 
   register_languages();
 
diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp
@@ -11,7 +11,6 @@ Author: Peter Schrammel
 
 #include "goto_diff_parse_options.h"
 
-#include <climits>
 #include <cstdlib> // exit()
 #include <fstream>
 #include <iostream>
@@ -135,13 +134,7 @@ int goto_diff_parse_optionst::doit()
   messaget::eval_verbosity(
     cmdline.get_value("verbosity"), messaget::M_STATISTICS, ui_message_handler);
 
-  //
-  // Print a banner
-  //
-  log.status() << "GOTO-DIFF version " << CBMC_VERSION << " "
-               << sizeof(void *) * CHAR_BIT << "-bit "
-               << config.this_architecture() << " "
-               << config.this_operating_system() << messaget::eom;
+  log_version_and_architecture("GOTO-DIFF");
 
   if(cmdline.args.size()!=2)
   {
diff --git a/src/util/parse_options.cpp b/src/util/parse_options.cpp
@@ -21,10 +21,12 @@ Author: Daniel Kroening, kroening@kroening.com
 #endif
 
 #include "cmdline.h"
+#include "config.h"
 #include "exception_utils.h"
 #include "exit_codes.h"
 #include "signal_catcher.h"
 #include "string_utils.h"
+#include "version.h"
 
 parse_options_baset::parse_options_baset(
   const std::string &_optstring,
@@ -147,6 +149,15 @@ int parse_options_baset::main()
   }
 }
 
+void parse_options_baset::log_version_and_architecture(
+  const std::string &front_end)
+{
+  log.status() << front_end << " version " << CBMC_VERSION << " "
+               << sizeof(void *) * CHAR_BIT << "-bit "
+               << config.this_architecture() << " "
+               << config.this_operating_system() << messaget::eom;
+}
+
 std::string align_center_with_border(const std::string &text)
 {
   auto const total_length = std::size_t{63};
diff --git a/src/util/parse_options.h b/src/util/parse_options.h
@@ -35,6 +35,9 @@ class parse_options_baset
   virtual int main();
   virtual ~parse_options_baset() { }
 
+  /// Write version and system architecture to log.status().
+  void log_version_and_architecture(const std::string &front_end);
+
 private:
   bool parse_result;
 
