add centered git version to CBMC banner

Author: Matthias Güdemann

jbmc/src/janalyzer/janalyzer_parse_options.cpp

@@ -721,17 +721,11 @@ bool janalyzer_parse_optionst::process_goto_program(const optionst &options)
 /// display command line help
 void janalyzer_parse_optionst::help()
 {
-  std::cout << "\n"
-               "* * JANALYZER " CBMC_VERSION " - Copyright (C) 2017-2018 ";
-
-  std::cout << "(" << (sizeof(void *) * 8) << "-bit version)";
-
-  std::cout << " * *\n";
-
   // clang-format off
-  std::cout <<
+  std::cout << '\n' << banner_string("JANALYZER", CBMC_VERSION) << '\n'
+            <<
      /* NOLINTNEXTLINE(whitespace/line_length) */
-    "* *         JANALYZER " CBMC_VERSION " - Copyright (C) 2016-2018          * *\n"
+    "* *                   Copyright (C) 2016-2018                    * *\n"
     "* *                  Daniel Kroening, Diffblue                   * *\n"
     "* *                   [email protected]                      * *\n"
     "\n"

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -1067,15 +1067,10 @@ bool jbmc_parse_optionst::generate_function_body(
 /// display command line help
 void jbmc_parse_optionst::help()
 {
-  std::cout << "\n"
-               "* *   JBMC " CBMC_VERSION " - Copyright (C) 2001-2018 ";
-
-  std::cout << "(" << (sizeof(void *)*8) << "-bit version)";
-
-  std::cout << "   * *\n";
-
   // clang-format off
-  std::cout <<
+  std::cout << '\n' << banner_string("JBMC", CBMC_VERSION) << '\n'
+            <<
+    "* *                 Copyright (C) 2001-2018                 * *\n"
     "* *              Daniel Kroening, Edmund Clarke             * *\n"
     "* * Carnegie Mellon University, Computer Science Department * *\n"
     "* *                 [email protected]                   * *\n"

jbmc/src/jdiff/jdiff_parse_options.cpp

@@ -427,10 +427,9 @@ bool jdiff_parse_optionst::process_goto_program(
 void jdiff_parse_optionst::help()
 {
   // clang-format off
-  std::cout <<
-    "\n"
-    // NOLINTNEXTLINE(whitespace/line_length)
-    "* *           JDIFF " CBMC_VERSION " - Copyright (C) 2016-2018       * *\n"
+  std::cout << '\n' << banner_string("JDIFF", CBMC_VERSION) << '\n'
+            <<
+    "* *                Copyright (C) 2016-2018                  * *\n"
     "* *            Daniel Kroening, Peter Schrammel             * *\n"
     "* *                 [email protected]                   * *\n"
     "\n"

src/cbmc/cbmc_parse_options.cpp

@@ -866,15 +866,9 @@ bool cbmc_parse_optionst::process_goto_program(
 void cbmc_parse_optionst::help()
 {
   // clang-format off
-  std::cout <<
-    "\n"
-    "* *   CBMC " CBMC_VERSION " - Copyright (C) 2001-2018 ";
-
-  std::cout << "(" << (sizeof(void *)*8) << "-bit version)";
-
-  std::cout << "   * *\n";
-
-  std::cout <<
+  std::cout << '\n' << banner_string("CBMC", CBMC_VERSION) << '\n'
+            <<
+    "* *                 Copyright (C) 2001-2018                 * *\n"
     "* *              Daniel Kroening, Edmund Clarke             * *\n"
     "* * Carnegie Mellon University, Computer Science Department * *\n"
     "* *                 [email protected]                   * *\n"

src/clobber/clobber_parse_options.cpp

@@ -348,15 +348,10 @@ void clobber_parse_optionst::report_failure()
 /// display command line help
 void clobber_parse_optionst::help()
 {
-  std::cout <<
-    "\n"
-    "* *     CLOBBER " CBMC_VERSION " - Copyright (C) 2014 ";
-
-  std::cout << "(" << (sizeof(void *)*8) << "-bit version)";
-
-  std::cout << "     * *\n";
-
-  std::cout <<
+  // clang-format off
+  std::cout << '\n' << banner_string("CLOBBER", CBMC_VERSION) << '\n'
+            <<
+    "* *                   Copyright (C) 2014                    * *\n"
     "* *                    Daniel Kroening                      * *\n"
     "* *                 University of Oxford                    * *\n"
     "* *                 [email protected]                   * *\n"
@@ -414,4 +409,5 @@ void clobber_parse_optionst::help()
     " --version                    show version and exit\n"
     " --xml-ui                     use XML-formatted output\n"
     "\n";
+  // clang-format on
 }

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -789,15 +789,10 @@ bool goto_analyzer_parse_optionst::process_goto_program(
 /// display command line help
 void goto_analyzer_parse_optionst::help()
 {
-  std::cout << "\n"
-               "* * GOTO-ANALYZER " CBMC_VERSION " - Copyright (C) 2017-2018 ";
-
-  std::cout << "(" << (sizeof(void *)*8) << "-bit version)";
-
-  std::cout << " * *\n";
-
   // clang-format off
-  std::cout <<
+  std::cout << '\n' << banner_string("GOTO-ANALYZER", CBMC_VERSION) << '\n'
+            <<
+    "* *                   Copyright (C) 2017-2018                    * *\n"
     "* *                  Daniel Kroening, DiffBlue                   * *\n"
     "* *                   [email protected]                      * *\n"
     "\n"

src/goto-cc/goto_cc_mode.cpp

@@ -22,6 +22,7 @@ Author: CM Wintersteiger, 2006
 #include <sysexits.h>
 #endif
 
+#include <util/parse_options.h>
 
 /// constructor
 goto_cc_modet::goto_cc_modet(
@@ -43,10 +44,10 @@ goto_cc_modet::~goto_cc_modet()
 /// display command line help
 void goto_cc_modet::help()
 {
-  std::cout <<
-  "\n"
-  // NOLINTNEXTLINE(whitespace/line_length)
-  "* *         goto-cc " CBMC_VERSION " - Copyright (C) 2006-2018           * *\n"
+  // clang-format off
+  std::cout << '\n' << banner_string("goto-cc", CBMC_VERSION) << '\n'
+            <<
+  "* *               Copyright (C) 2006-2018                   * *\n"
   "* *          Daniel Kroening, Michael Tautschnig,           * *\n"
   "* *               Christoph Wintersteiger                   * *\n"
   "\n";
@@ -64,6 +65,7 @@ void goto_cc_modet::help()
   " --print-rejected-preprocessed-source file\n"
   "                             copy failing (preprocessed) source to file\n"
   "\n";
+  // clang-format on
 }
 
 /// starts the compiler

src/goto-diff/goto_diff_parse_options.cpp

@@ -484,10 +484,9 @@ bool goto_diff_parse_optionst::process_goto_program(
 void goto_diff_parse_optionst::help()
 {
   // clang-format off
-  std::cout <<
-    "\n"
-    // NOLINTNEXTLINE(whitespace/line_length)
-    "* *           GOTO_DIFF " CBMC_VERSION " - Copyright (C) 2016            * *\n"
+  std::cout << '\n' << banner_string("GOTO_DIFF", CBMC_VERSION) << '\n'
+            <<
+    "* *                  Copyright (C) 2016                     * *\n"
     "* *            Daniel Kroening, Peter Schrammel             * *\n"
     "* *                 [email protected]                   * *\n"
     "\n"

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1439,9 +1439,9 @@ void goto_instrument_parse_optionst::instrument_goto_program()
 void goto_instrument_parse_optionst::help()
 {
   // clang-format off
-  std::cout <<
-    "\n"
-    "* *     Goto-Instrument " CBMC_VERSION " - Copyright (C) 2008-2013       * *\n" // NOLINT(*)
+  std::cout << '\n' << banner_string("Goto-Instrument", CBMC_VERSION) << '\n'
+            <<
+    "* *                Copyright (C) 2008-2013                  * *\n"
     "* *                    Daniel Kroening                      * *\n"
     "* *                 [email protected]                   * *\n"
     "\n"

src/memory-models/mmcc_parse_options.cpp

@@ -95,16 +95,16 @@ int mmcc_parse_optionst::convert(
 /// display command line help
 void mmcc_parse_optionst::help()
 {
-  std::cout <<
-    "\n"
-    "* *   MMCC " CBMC_VERSION " - Copyright (C) 2015-2015    * *\n";
-
-  std::cout <<
+  // clang-format off
+  std::cout << '\n' << banner_string("MMCC", CBMC_VERSION) << '\n'
+            <<
+    "                  Copyright (C) 2015-2015\n"
     "\n"
     "Usage:                       Purpose:\n"
     "\n"
     " mmcc [-?] [-h] [--help]      show help\n"
     " mmcc file.cat                convert given source file\n"
     " mmcc                         convert from stdin\n"
     "\n";
+  // clang-format on
 }

src/util/parse_options.cpp

@@ -65,3 +65,20 @@ int parse_options_baset::main()
 
   return doit();
 }
+
+std::string
+banner_string(const std::string &front_end, const std::string &version)
+{
+  const std::string version_str = front_end + " " + version + " " +
+                                  std::to_string(sizeof(void *) * 8) + "-bit";
+
+  std::string::size_type left_padding = 0, right_padding = 0;
+  if(version_str.size() < 57)
+  {
+    left_padding = (57 - version_str.size() + 1) / 2;
+    right_padding = (57 - version_str.size()) / 2;
+  }
+
+  return "* *" + std::string(left_padding, ' ') + version_str +
+         std::string(right_padding, ' ') + "* *";
+}

src/util/parse_options.h

@@ -35,4 +35,7 @@ class parse_options_baset
   bool parse_result;
 };
 
+std::string
+banner_string(const std::string &front_end, const std::string &version);
+
 #endif // CPROVER_UTIL_PARSE_OPTIONS_H