Skip to content

Commit f6f7ecd

Browse files
NlightNFotisNlightNFotis
authored
Merge pull request #3920 from hannes-steffenhagen-diffblue/feature-banner_helper
Feature banner helper
2 parents 4eb7d04 + b7a33ba commit f6f7ecd

12 files changed

+71
-40
lines changed

‎jbmc/src/janalyzer/janalyzer_parse_options.cpp

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -736,11 +736,10 @@ void janalyzer_parse_optionst::help()
736736
{
737737
// clang-format off
738738
std::cout << '\n' << banner_string("JANALYZER", CBMC_VERSION) << '\n'
739+
<< align_center_with_border("Copyright (C) 2016-2018") << '\n'
740+
<< align_center_with_border("Daniel Kroening, Diffblue") << '\n'
741+
<< align_center_with_border("[email protected]") << '\n'
739742
<<
740-
/* NOLINTNEXTLINE(whitespace/line_length) */
741-
"* * Copyright (C) 2016-2018 * *\n"
742-
"* * Daniel Kroening, Diffblue * *\n"
743-
"* * [email protected] * *\n"
744743
"\n"
745744
"Usage: Purpose:\n"
746745
"\n"

‎jbmc/src/jbmc/jbmc_parse_options.cpp

Lines changed: 5 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1094,12 +1094,11 @@ void jbmc_parse_optionst::help()
10941094
{
10951095
// clang-format off
10961096
std::cout << '\n' << banner_string("JBMC", CBMC_VERSION) << '\n'
1097-
<<
1098-
"* * Copyright (C) 2001-2018 * *\n"
1099-
"* * Daniel Kroening, Edmund Clarke * *\n"
1100-
"* * Carnegie Mellon University, Computer Science Department * *\n"
1101-
"* * [email protected] * *\n"
1102-
"\n"
1097+
<< align_center_with_border("Copyright (C) 2001-2018") << '\n'
1098+
<< align_center_with_border("Daniel Kroening, Edmund Clarke") << '\n' // NOLINT(*)
1099+
<< align_center_with_border("Carnegie Mellon University, Computer Science Department") << '\n' // NOLINT(*)
1100+
<< align_center_with_border("[email protected]") << '\n'
1101+
<< "\n"
11031102
"Usage: Purpose:\n"
11041103
"\n"
11051104
" jbmc [-?] [-h] [--help] show help\n"

‎jbmc/src/jdiff/jdiff_parse_options.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -440,10 +440,10 @@ void jdiff_parse_optionst::help()
440440
{
441441
// clang-format off
442442
std::cout << '\n' << banner_string("JDIFF", CBMC_VERSION) << '\n'
443+
<< align_center_with_border("Copyright (C) 2016-2018") << '\n'
444+
<< align_center_with_border("Daniel Kroening, Peter Schrammel") << '\n' // NOLINT(*)
445+
<< align_center_with_border("[email protected]") << '\n'
443446
<<
444-
"* * Copyright (C) 2016-2018 * *\n"
445-
"* * Daniel Kroening, Peter Schrammel * *\n"
446-
"* * [email protected] * *\n"
447447
"\n"
448448
"Usage: Purpose:\n"
449449
"\n"

‎src/cbmc/cbmc_parse_options.cpp

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -796,12 +796,12 @@ void cbmc_parse_optionst::help()
796796
{
797797
// clang-format off
798798
std::cout << '\n' << banner_string("CBMC", CBMC_VERSION) << '\n'
799+
<< align_center_with_border("Copyright (C) 2001-2018") << '\n'
800+
<< align_center_with_border("Daniel Kroening, Edmund Clarke") << '\n' // NOLINT(*)
801+
<< align_center_with_border("Carnegie Mellon University, Computer Science Department") << '\n' // NOLINT(*)
802+
<< align_center_with_border("[email protected]") << '\n' // NOLINT(*)
803+
<< align_center_with_border("Protected in part by U.S. patent 7,225,417") << '\n' // NOLINT(*)
799804
<<
800-
"* * Copyright (C) 2001-2018 * *\n"
801-
"* * Daniel Kroening, Edmund Clarke * *\n"
802-
"* * Carnegie Mellon University, Computer Science Department * *\n"
803-
"* * [email protected] * *\n"
804-
"* * Protected in part by U.S. patent 7,225,417 * *\n"
805805
"\n"
806806
"Usage: Purpose:\n"
807807
"\n"

‎src/goto-analyzer/goto_analyzer_parse_options.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -717,10 +717,10 @@ void goto_analyzer_parse_optionst::help()
717717
{
718718
// clang-format off
719719
std::cout << '\n' << banner_string("GOTO-ANALYZER", CBMC_VERSION) << '\n'
720+
<< align_center_with_border("Copyright (C) 2017-2018") << '\n'
721+
<< align_center_with_border("Daniel Kroening, Diffblue") << '\n'
722+
<< align_center_with_border("[email protected]") << '\n'
720723
<<
721-
"* * Copyright (C) 2017-2018 * *\n"
722-
"* * Daniel Kroening, Diffblue * *\n"
723-
"* * [email protected] * *\n"
724724
"\n"
725725
"Usage: Purpose:\n"
726726
"\n"

‎src/goto-cc/goto_cc_mode.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -48,10 +48,10 @@ void goto_cc_modet::help()
4848
{
4949
// clang-format off
5050
std::cout << '\n' << banner_string("goto-cc", CBMC_VERSION) << '\n'
51+
<< align_center_with_border("Copyright (C) 2006-2018") << '\n'
52+
<< align_center_with_border("Daniel Kroening, Michael Tautschnig,") << '\n' // NOLINT(*)
53+
<< align_center_with_border("Christoph Wintersteiger") << '\n'
5154
<<
52-
"* * Copyright (C) 2006-2018 * *\n"
53-
"* * Daniel Kroening, Michael Tautschnig, * *\n"
54-
"* * Christoph Wintersteiger * *\n"
5555
"\n";
5656

5757
help_mode();

‎src/goto-diff/goto_diff_parse_options.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -457,10 +457,10 @@ void goto_diff_parse_optionst::help()
457457
{
458458
// clang-format off
459459
std::cout << '\n' << banner_string("GOTO_DIFF", CBMC_VERSION) << '\n'
460+
<< align_center_with_border("Copyright (C) 2016") << '\n'
461+
<< align_center_with_border("Daniel Kroening, Peter Schrammel") << '\n' // NOLINT (*)
462+
<< align_center_with_border("[email protected]") << '\n'
460463
<<
461-
"* * Copyright (C) 2016 * *\n"
462-
"* * Daniel Kroening, Peter Schrammel * *\n"
463-
"* * [email protected] * *\n"
464464
"\n"
465465
"Usage: Purpose:\n"
466466
"\n"

‎src/goto-instrument/goto_instrument_parse_options.cpp

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1532,10 +1532,10 @@ void goto_instrument_parse_optionst::help()
15321532
{
15331533
// clang-format off
15341534
std::cout << '\n' << banner_string("Goto-Instrument", CBMC_VERSION) << '\n'
1535+
<< align_center_with_border("Copyright (C) 2008-2013") << '\n'
1536+
<< align_center_with_border("Daniel Kroening") << '\n'
1537+
<< align_center_with_border("[email protected]") << '\n'
15351538
<<
1536-
"* * Copyright (C) 2008-2013 * *\n"
1537-
"* * Daniel Kroening * *\n"
1538-
"* * [email protected] * *\n"
15391539
"\n"
15401540
"Usage: Purpose:\n"
15411541
"\n"

‎src/util/parse_options.cpp

Lines changed: 17 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,8 @@ Author: Daniel Kroening, [email protected]
88

99
#include "parse_options.h"
1010

11+
#include <algorithm>
12+
#include <climits>
1113
#include <iostream>
1214

1315
#if defined (_WIN32)
@@ -116,19 +118,24 @@ int parse_options_baset::main()
116118
}
117119
}
118120

121+
std::string align_center_with_border(const std::string &text)
122+
{
123+
auto const total_length = std::size_t{63};
124+
auto const border = std::string{"* *"};
125+
auto const fill =
126+
total_length - std::min(total_length, 2 * border.size() + text.size());
127+
auto const fill_right = fill / 2;
128+
auto const fill_left = fill - fill_right;
129+
return border + std::string(fill_left, ' ') + text +
130+
std::string(fill_right, ' ') + border;
131+
}
132+
119133
std::string
120134
banner_string(const std::string &front_end, const std::string &version)
121135
{
122136
const std::string version_str = front_end + " " + version + " " +
123-
std::to_string(sizeof(void *) * 8) + "-bit";
124-
125-
std::string::size_type left_padding = 0, right_padding = 0;
126-
if(version_str.size() < 57)
127-
{
128-
left_padding = (57 - version_str.size() + 1) / 2;
129-
right_padding = (57 - version_str.size()) / 2;
130-
}
137+
std::to_string(sizeof(void *) * CHAR_BIT) +
138+
"-bit";
131139

132-
return "* *" + std::string(left_padding, ' ') + version_str +
133-
std::string(right_padding, ' ') + "* *";
140+
return align_center_with_border(version_str);
134141
}

‎src/util/parse_options.h

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -38,4 +38,12 @@ class parse_options_baset
3838
std::string
3939
banner_string(const std::string &front_end, const std::string &version);
4040

41+
/// Utility for displaying help centered messages borderered by "* *"
42+
/// - we use this for displaying banner information and the like
43+
/// in help messages
44+
/// \example
45+
/// align_center_with_border("test-text")
46+
/// == "* * test-text * *"
47+
std::string align_center_with_border(const std::string &text);
48+
4149
#endif // CPROVER_UTIL_PARSE_OPTIONS_H

‎unit/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -56,6 +56,7 @@ SRC += analyses/ai/ai.cpp \
5656
util/message.cpp \
5757
util/optional.cpp \
5858
util/optional_utils.cpp \
59+
util/parse_options.cpp \
5960
util/pointer_offset_size.cpp \
6061
util/range.cpp \
6162
util/replace_symbol.cpp \

‎unit/util/parse_options.cpp

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
/******************************************************************\
2+
3+
Module: parse_options unit tests
4+
5+
Author: Diffblue Ltd.
6+
7+
\******************************************************************/
8+
9+
#include <testing-utils/use_catch.h>
10+
#include <util/parse_options.h>
11+
12+
TEST_CASE("align_center_with_border", "[core][util]")
13+
{
14+
REQUIRE(
15+
align_center_with_border("test-text") ==
16+
"* * test-text * *");
17+
}

0 commit comments

Comments
 (0)