Feature banner helper

jbmc/src/janalyzer/janalyzer_parse_options.cpp

@@ -736,11 +736,10 @@ void janalyzer_parse_optionst::help()
 {
   // clang-format off
   std::cout << '\n' << banner_string("JANALYZER", CBMC_VERSION) << '\n'
+            << align_center_with_border("Copyright (C) 2016-2018") << '\n'
+            << align_center_with_border("Daniel Kroening, Diffblue") << '\n'
+            << align_center_with_border("[email protected]") << '\n'
             <<
-     /* NOLINTNEXTLINE(whitespace/line_length) */
-    "* *                   Copyright (C) 2016-2018                    * *\n"
-    "* *                  Daniel Kroening, Diffblue                   * *\n"
-    "* *                   [email protected]                      * *\n"
     "\n"
     "Usage:                       Purpose:\n"
     "\n"

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -1094,12 +1094,11 @@ void jbmc_parse_optionst::help()
 {
   // clang-format off
   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"
-    "\n"
+            << align_center_with_border("Copyright (C) 2001-2018") << '\n'
+            << align_center_with_border("Daniel Kroening, Edmund Clarke") << '\n' // NOLINT(*)
+            << align_center_with_border("Carnegie Mellon University, Computer Science Department") << '\n' // NOLINT(*)
+            << align_center_with_border("[email protected]") << '\n'
+            << "\n"
     "Usage:                       Purpose:\n"
     "\n"
     " jbmc [-?] [-h] [--help]      show help\n"

jbmc/src/jdiff/jdiff_parse_options.cpp

@@ -440,10 +440,10 @@ void jdiff_parse_optionst::help()
 {
   // clang-format off
   std::cout << '\n' << banner_string("JDIFF", CBMC_VERSION) << '\n'
+            << align_center_with_border("Copyright (C) 2016-2018") << '\n'
+            << align_center_with_border("Daniel Kroening, Peter Schrammel") << '\n' // NOLINT(*)
+            << align_center_with_border("[email protected]") << '\n'
             <<
-    "* *                Copyright (C) 2016-2018                  * *\n"
-    "* *            Daniel Kroening, Peter Schrammel             * *\n"
-    "* *                 [email protected]                   * *\n"
     "\n"
     "Usage:                       Purpose:\n"
     "\n"

src/cbmc/cbmc_parse_options.cpp

@@ -796,12 +796,12 @@ void cbmc_parse_optionst::help()
 {
   // clang-format off
   std::cout << '\n' << banner_string("CBMC", CBMC_VERSION) << '\n'
+            << align_center_with_border("Copyright (C) 2001-2018") << '\n'
+            << align_center_with_border("Daniel Kroening, Edmund Clarke") << '\n' // NOLINT(*)
+            << align_center_with_border("Carnegie Mellon University, Computer Science Department") << '\n' // NOLINT(*)
+            << align_center_with_border("[email protected]") << '\n' // NOLINT(*)
+            << align_center_with_border("Protected in part by U.S. patent 7,225,417") << '\n' // NOLINT(*)
             <<
-    "* *                 Copyright (C) 2001-2018                 * *\n"
-    "* *              Daniel Kroening, Edmund Clarke             * *\n"
-    "* * Carnegie Mellon University, Computer Science Department * *\n"
-    "* *                 [email protected]                   * *\n"
-    "* *        Protected in part by U.S. patent 7,225,417       * *\n"
     "\n"
     "Usage:                       Purpose:\n"
     "\n"

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -717,10 +717,10 @@ void goto_analyzer_parse_optionst::help()
 {
   // clang-format off
   std::cout << '\n' << banner_string("GOTO-ANALYZER", CBMC_VERSION) << '\n'
+            << align_center_with_border("Copyright (C) 2017-2018") << '\n'
+            << align_center_with_border("Daniel Kroening, Diffblue") << '\n'
+            << align_center_with_border("[email protected]") << '\n'
             <<
-    "* *                   Copyright (C) 2017-2018                    * *\n"
-    "* *                  Daniel Kroening, Diffblue                   * *\n"
-    "* *                   [email protected]                      * *\n"
     "\n"
     "Usage:                       Purpose:\n"
     "\n"

src/goto-cc/goto_cc_mode.cpp

@@ -48,10 +48,10 @@ void goto_cc_modet::help()
 {
   // clang-format off
   std::cout << '\n' << banner_string("goto-cc", CBMC_VERSION) << '\n'
+            << align_center_with_border("Copyright (C) 2006-2018") << '\n'
+            << align_center_with_border("Daniel Kroening, Michael Tautschnig,") << '\n' // NOLINT(*)
+            << align_center_with_border("Christoph Wintersteiger") << '\n'
             <<
-  "* *               Copyright (C) 2006-2018                   * *\n"
-  "* *          Daniel Kroening, Michael Tautschnig,           * *\n"
-  "* *               Christoph Wintersteiger                   * *\n"
   "\n";
 
   help_mode();

src/goto-diff/goto_diff_parse_options.cpp

@@ -457,10 +457,10 @@ void goto_diff_parse_optionst::help()
 {
   // clang-format off
   std::cout << '\n' << banner_string("GOTO_DIFF", CBMC_VERSION) << '\n'
+            << align_center_with_border("Copyright (C) 2016") << '\n'
+            << align_center_with_border("Daniel Kroening, Peter Schrammel") << '\n' // NOLINT (*)
+            << align_center_with_border("[email protected]") << '\n'
             <<
-    "* *                  Copyright (C) 2016                     * *\n"
-    "* *            Daniel Kroening, Peter Schrammel             * *\n"
-    "* *                 [email protected]                   * *\n"
     "\n"
     "Usage:                       Purpose:\n"
     "\n"

src/goto-instrument/goto_instrument_parse_options.cpp

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

src/util/parse_options.cpp

@@ -8,6 +8,8 @@ Author: Daniel Kroening, [email protected]
 
 #include "parse_options.h"
 
+#include <algorithm>
+#include <climits>
 #include <iostream>
 
 #if defined (_WIN32)
@@ -116,19 +118,24 @@ int parse_options_baset::main()
   }
 }
 
+std::string align_center_with_border(const std::string &text)
+{
+  auto const total_length = std::size_t{63};
+  auto const border = std::string{"* *"};
+  auto const fill =
+    total_length - std::min(total_length, 2 * border.size() + text.size());
+  auto const fill_right = fill / 2;
+  auto const fill_left = fill - fill_right;
+  return border + std::string(fill_left, ' ') + text +
+         std::string(fill_right, ' ') + border;
+}
+
 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;
-  }
+                                  std::to_string(sizeof(void *) * CHAR_BIT) +
+                                  "-bit";
 
-  return "* *" + std::string(left_padding, ' ') + version_str +
-         std::string(right_padding, ' ') + "* *";
+  return align_center_with_border(version_str);
 }

src/util/parse_options.h

@@ -38,4 +38,12 @@ class parse_options_baset
 std::string
 banner_string(const std::string &front_end, const std::string &version);
 
+/// Utility for displaying help centered messages borderered by "* *"
+/// - we use this for displaying banner information and the like
+/// in help messages
+/// \example
+///   align_center_with_border("test-text")
+///   == "* *                        test-text                        * *"
+std::string align_center_with_border(const std::string &text);
+
 #endif // CPROVER_UTIL_PARSE_OPTIONS_H

unit/Makefile

@@ -56,6 +56,7 @@ SRC += analyses/ai/ai.cpp \
        util/message.cpp \
        util/optional.cpp \
        util/optional_utils.cpp \
+       util/parse_options.cpp \
        util/pointer_offset_size.cpp \
        util/range.cpp \
        util/replace_symbol.cpp \

unit/util/parse_options.cpp

@@ -0,0 +1,17 @@
+/******************************************************************\
+
+Module: parse_options unit tests
+
+Author: Diffblue Ltd.
+
+\******************************************************************/
+
+#include <testing-utils/use_catch.h>
+#include <util/parse_options.h>
+
+TEST_CASE("align_center_with_border", "[core][util]")
+{
+  REQUIRE(
+    align_center_with_border("test-text") ==
+    "* *                        test-text                        * *");
+}