diff --git a/jbmc/src/janalyzer/janalyzer_parse_options.cpp b/jbmc/src/janalyzer/janalyzer_parse_options.cpp index 26feac02184..90fc5790998 100644 --- a/jbmc/src/janalyzer/janalyzer_parse_options.cpp +++ b/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("kroening@kroening.com") << '\n' << - /* NOLINTNEXTLINE(whitespace/line_length) */ - "* * Copyright (C) 2016-2018 * *\n" - "* * Daniel Kroening, Diffblue * *\n" - "* * kroening@kroening.com * *\n" "\n" "Usage: Purpose:\n" "\n" diff --git a/jbmc/src/jbmc/jbmc_parse_options.cpp b/jbmc/src/jbmc/jbmc_parse_options.cpp index 1e175a0489e..4ab56be7ee1 100644 --- a/jbmc/src/jbmc/jbmc_parse_options.cpp +++ b/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" - "* * kroening@kroening.com * *\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("kroening@kroening.com") << '\n' + << "\n" "Usage: Purpose:\n" "\n" " jbmc [-?] [-h] [--help] show help\n" diff --git a/jbmc/src/jdiff/jdiff_parse_options.cpp b/jbmc/src/jdiff/jdiff_parse_options.cpp index 8b6acc24d75..683a8d1f7c7 100644 --- a/jbmc/src/jdiff/jdiff_parse_options.cpp +++ b/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("kroening@kroening.com") << '\n' << - "* * Copyright (C) 2016-2018 * *\n" - "* * Daniel Kroening, Peter Schrammel * *\n" - "* * kroening@kroening.com * *\n" "\n" "Usage: Purpose:\n" "\n" diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index c72826326d9..b1407a5d71e 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/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("kroening@kroening.com") << '\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" - "* * kroening@kroening.com * *\n" - "* * Protected in part by U.S. patent 7,225,417 * *\n" "\n" "Usage: Purpose:\n" "\n" diff --git a/src/goto-analyzer/goto_analyzer_parse_options.cpp b/src/goto-analyzer/goto_analyzer_parse_options.cpp index 0487e82211c..a54e6f8b0a5 100644 --- a/src/goto-analyzer/goto_analyzer_parse_options.cpp +++ b/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("kroening@kroening.com") << '\n' << - "* * Copyright (C) 2017-2018 * *\n" - "* * Daniel Kroening, Diffblue * *\n" - "* * kroening@kroening.com * *\n" "\n" "Usage: Purpose:\n" "\n" diff --git a/src/goto-cc/goto_cc_mode.cpp b/src/goto-cc/goto_cc_mode.cpp index 59cebe82e2f..f7b705a15b3 100644 --- a/src/goto-cc/goto_cc_mode.cpp +++ b/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(); diff --git a/src/goto-diff/goto_diff_parse_options.cpp b/src/goto-diff/goto_diff_parse_options.cpp index 0edca2feebc..5342c761ce0 100644 --- a/src/goto-diff/goto_diff_parse_options.cpp +++ b/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("kroening@kroening.com") << '\n' << - "* * Copyright (C) 2016 * *\n" - "* * Daniel Kroening, Peter Schrammel * *\n" - "* * kroening@kroening.com * *\n" "\n" "Usage: Purpose:\n" "\n" diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index ce2ca697688..867e514010d 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/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("kroening@kroening.com") << '\n' << - "* * Copyright (C) 2008-2013 * *\n" - "* * Daniel Kroening * *\n" - "* * kroening@kroening.com * *\n" "\n" "Usage: Purpose:\n" "\n" diff --git a/src/util/parse_options.cpp b/src/util/parse_options.cpp index 5c1db010b2e..1b556f85c3f 100644 --- a/src/util/parse_options.cpp +++ b/src/util/parse_options.cpp @@ -8,6 +8,8 @@ Author: Daniel Kroening, kroening@kroening.com #include "parse_options.h" +#include +#include #include #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); } diff --git a/src/util/parse_options.h b/src/util/parse_options.h index 6b2b982fd51..304657c6879 100644 --- a/src/util/parse_options.h +++ b/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 diff --git a/unit/Makefile b/unit/Makefile index bc2e452bca6..fd1e8d30ec1 100644 --- a/unit/Makefile +++ b/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 \ diff --git a/unit/util/parse_options.cpp b/unit/util/parse_options.cpp new file mode 100644 index 00000000000..697cbe885fc --- /dev/null +++ b/unit/util/parse_options.cpp @@ -0,0 +1,17 @@ +/******************************************************************\ + +Module: parse_options unit tests + +Author: Diffblue Ltd. + +\******************************************************************/ + +#include +#include + +TEST_CASE("align_center_with_border", "[core][util]") +{ + REQUIRE( + align_center_with_border("test-text") == + "* * test-text * *"); +}