diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 6f780755c7b..9a3d00a69b4 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1799,7 +1799,7 @@ void goto_instrument_parse_optionst::help() " --race-check add floating-point data race checks\n" "\n" "Semantic transformations:\n" - HELP_NONDET_VOLATILE + << HELP_NONDET_VOLATILE << " --unwind unwinds the loops times\n" " --unwindset L:B,... unwind loop L with a bound of B\n" " --unwindset-file read unwindset from file\n" diff --git a/src/goto-instrument/nondet_volatile.h b/src/goto-instrument/nondet_volatile.h index dc12bf83551..e0045a418bf 100644 --- a/src/goto-instrument/nondet_volatile.h +++ b/src/goto-instrument/nondet_volatile.h @@ -28,14 +28,15 @@ class optionst; "(" NONDET_VOLATILE_MODEL_OPT "):" #define HELP_NONDET_VOLATILE \ - " --" NONDET_VOLATILE_OPT " makes reads from volatile variables " \ - "non-deterministic\n" \ - " --" NONDET_VOLATILE_VARIABLE_OPT " \n" \ - " makes reads from given volatile variable " \ - "non-deterministic\n" \ - " --" NONDET_VOLATILE_MODEL_OPT ":\n" \ - " models reads from given volatile variable " \ - "by a call to the given model" + help_entry( \ + "--" NONDET_VOLATILE_OPT, \ + "makes reads from volatile variables non-deterministic") << \ + help_entry( \ + "--" NONDET_VOLATILE_VARIABLE_OPT " ", \ + "makes reads from given volatile variable non-deterministic") << \ + help_entry( \ + "--" NONDET_VOLATILE_MODEL_OPT " :", \ + "models reads from given volatile variable by a call to the given model") // clang-format on void parse_nondet_volatile_options(const cmdlinet &cmdline, optionst &options); diff --git a/src/util/parse_options.cpp b/src/util/parse_options.cpp index d9dbdac6e48..4e083e59bb5 100644 --- a/src/util/parse_options.cpp +++ b/src/util/parse_options.cpp @@ -9,6 +9,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "parse_options.h" #include +#include #include #include @@ -23,6 +24,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "exception_utils.h" #include "exit_codes.h" #include "signal_catcher.h" +#include "string_utils.h" parse_options_baset::parse_options_baset( const std::string &_optstring, @@ -151,3 +153,54 @@ banner_string(const std::string &front_end, const std::string &version) return align_center_with_border(version_str); } + +std::string help_entry( + const std::string &option, + const std::string &description, + const std::size_t left_margin, + const std::size_t width) +{ + PRECONDITION(!option.empty()); + PRECONDITION(!std::isspace(option.front())); + PRECONDITION(!std::isspace(option.back())); + PRECONDITION(option.length() <= width); + + PRECONDITION(!description.empty()); + PRECONDITION(!std::isspace(description.front())); + PRECONDITION(!std::isspace(description.back())); + + PRECONDITION(left_margin < width); + + std::string result; + + if(option.length() >= left_margin - 1) + { + result = " " + option + "\n"; + result += wrap_line(description, left_margin, width) + "\n"; + + return result; + } + + std::string padding(left_margin - option.length() - 1, ' '); + result = " " + option + padding; + + if(description.length() <= (width - left_margin)) + { + return result + description + "\n"; + } + + auto it = description.cbegin() + (width - left_margin); + auto rit = std::reverse_iterator(it) - 1; + + auto rit_space = std::find(rit, description.crend(), ' '); + auto it_space = rit_space.base() - 1; + CHECK_RETURN(*it_space == ' '); + + result.append(description.cbegin(), it_space); + result.append("\n"); + + result += + wrap_line(it_space + 1, description.cend(), left_margin, width) + "\n"; + + return result; +} diff --git a/src/util/parse_options.h b/src/util/parse_options.h index 6cfdbcf9ad9..b4ea02d720c 100644 --- a/src/util/parse_options.h +++ b/src/util/parse_options.h @@ -58,4 +58,10 @@ banner_string(const std::string &front_end, const std::string &version); /// ``` std::string align_center_with_border(const std::string &text); +std::string help_entry( + const std::string &option, + const std::string &description, + const std::size_t left_margin = 30, + const std::size_t width = 80); + #endif // CPROVER_UTIL_PARSE_OPTIONS_H diff --git a/src/util/string_utils.cpp b/src/util/string_utils.cpp index aab98943475..9763c657b5a 100644 --- a/src/util/string_utils.cpp +++ b/src/util/string_utils.cpp @@ -174,3 +174,75 @@ std::string capitalize(const std::string &str) capitalized[0] = toupper(capitalized[0]); return capitalized; } + +std::string wrap_line( + const std::string &line, + const std::size_t left_margin, + const std::size_t width) +{ + return wrap_line(line.cbegin(), line.cend(), left_margin, width); +} + +std::string wrap_line( + std::string::const_iterator left, + std::string::const_iterator right, + const std::size_t left_margin, + const std::size_t width) +{ + PRECONDITION(left_margin < width); + + const std::size_t column_width = width - left_margin; + const std::string margin(left_margin, ' '); + + auto distance = std::distance(left, right); + CHECK_RETURN(distance > 0); + + std::string result; + + if(static_cast(distance) <= column_width) + { + result.append(margin); + result.append(left, right); + + return result; + } + + auto it_line_begin = left; + + do + { + // points to the first character past the current column + auto it = it_line_begin + column_width; + + auto rit_r = std::reverse_iterator(it) - 1; + auto rit_l = rit_r + column_width; + + auto rit_space = std::find(rit_r, rit_l, ' '); + + if(rit_space != rit_l) + { + auto it_space = rit_space.base() - 1; + CHECK_RETURN(*it_space == ' '); + + result.append(margin); + result.append(it_line_begin, it_space); + result.append("\n"); + + it_line_begin = it_space + 1; + } + else + { + // we have not found a space, thus cannot wrap this line + result.clear(); + result.append(left, right); + + return result; + } + } while(static_cast(std::distance(it_line_begin, right)) > + column_width); + + result.append(margin); + result.append(it_line_begin, right); + + return result; +} diff --git a/src/util/string_utils.h b/src/util/string_utils.h index a73bd8bd9cd..d6e06f21d3f 100644 --- a/src/util/string_utils.h +++ b/src/util/string_utils.h @@ -108,4 +108,44 @@ std::string escape(const std::string &); /// \return string with non-alphanumeric characters escaped std::string escape_non_alnum(const std::string &to_escape); +/// Wrap line at spaces to not extend past the right margin, and include given +/// padding with spaces to the left +/// +/// The given string should not contain any newlines. +/// +/// \param line: line to wrap, should not contain newlines +/// \param left_margin: each line will be padded to the left with `left_margin` +/// spaces +/// \param width: width of the resulting text, i.e., right margin +/// \return resulting string such that each line has length less or equal to +/// `width`, and each line includes `left_margin` spaces to the left; if the +/// given line cannot be wrapped (i.e., it cannot be broken up at spaces such +/// that every resulting line fits within the margin), the given line is +/// returned unchanged +std::string wrap_line( + const std::string &line, + const std::size_t left_margin = 0, + const std::size_t width = 80); + +/// Wrap line at spaces to not extend past the right margin, and include given +/// padding with spaces to the left +/// +/// The given string should not contain any newlines. +/// +/// \param left: iterator to beginning of string +/// \param right: iterator to end of string +/// \param left_margin: each line will be padded to the left with `left_margin` +/// spaces +/// \param width: width of the resulting text, i.e., right margin +/// \return resulting string such that each line has length less or equal to +/// `width`, and each line includes `left_margin` spaces to the left; if the +/// given line cannot be wrapped (i.e., it cannot be broken up at spaces such +/// that every resulting line fits within the margin), the given line is +/// returned unchanged +std::string wrap_line( + const std::string::const_iterator left, + const std::string::const_iterator right, + const std::size_t left_margin = 0, + const std::size_t width = 80); + #endif diff --git a/unit/Makefile b/unit/Makefile index f581bb010bf..e30aaf506f9 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -117,6 +117,7 @@ SRC += analyses/ai/ai.cpp \ util/string_utils/join_string.cpp \ util/string_utils/split_string.cpp \ util/string_utils/strip_string.cpp \ + util/string_utils/wrap_line.cpp \ util/symbol_table.cpp \ util/symbol.cpp \ util/unicode.cpp \ diff --git a/unit/util/parse_options.cpp b/unit/util/parse_options.cpp index 697cbe885fc..603671fdf3f 100644 --- a/unit/util/parse_options.cpp +++ b/unit/util/parse_options.cpp @@ -15,3 +15,12 @@ TEST_CASE("align_center_with_border", "[core][util]") align_center_with_border("test-text") == "* * test-text * *"); } + +TEST_CASE("help_entry", "[core][util]") +{ + REQUIRE(help_entry("--abc", "xyz", 8, 12) == " --abc xyz\n"); + REQUIRE(help_entry("--abc", "xxxx x", 8, 12) == " --abc xxxx\n x\n"); + REQUIRE(help_entry("--abc", "xx xx", 8, 12) == " --abc xx\n xx\n"); + REQUIRE(help_entry("--abcdef", "xyz", 8, 12) == " --abcdef\n xyz\n"); + REQUIRE(help_entry("--abcdefg", "xyz", 8, 12) == " --abcdefg\n xyz\n"); +} diff --git a/unit/util/string_utils/wrap_line.cpp b/unit/util/string_utils/wrap_line.cpp new file mode 100644 index 00000000000..0c27996f341 --- /dev/null +++ b/unit/util/string_utils/wrap_line.cpp @@ -0,0 +1,32 @@ +/// Author: Daniel Poetzl + +/// \file Tests for wrap_line() + +#include +#include + +TEST_CASE("Wrap line", "[core][util]") +{ + SECTION("Wrap without margin") + { + REQUIRE(wrap_line("x", 0, 1) == "x"); + REQUIRE(wrap_line("x x", 0, 1) == "x\nx"); + REQUIRE(wrap_line("x x x", 0, 1) == "x\nx\nx"); + + REQUIRE(wrap_line("x x", 0, 2) == "x\nx"); + REQUIRE(wrap_line("xx xx xx", 0, 4) == "xx\nxx\nxx"); + + REQUIRE(wrap_line("xx", 0, 1) == "xx"); + } + + SECTION("Wrap with margin") + { + REQUIRE(wrap_line("x", 1, 2) == " x"); + REQUIRE(wrap_line("x x", 1, 2) == " x\n x"); + REQUIRE(wrap_line("x x x", 1, 2) == " x\n x\n x"); + + REQUIRE(wrap_line("x", 2, 3) == " x"); + + REQUIRE(wrap_line("xx", 1, 2) == "xx"); + } +}