Fix format of nondet volatile command line help

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 <n>                 unwinds the loops <n> times\n"
     " --unwindset L:B,...          unwind loop L with a bound of B\n"
     " --unwindset-file <file>      read unwindset from file\n"

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 " <variable>\n" \
-  "                              makes reads from given volatile variable " \
-  "non-deterministic\n" \
-  " --" NONDET_VOLATILE_MODEL_OPT "<variable>:<model>\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 " <variable>", \
+    "makes reads from given volatile variable non-deterministic") << \
+  help_entry( \
+    "--" NONDET_VOLATILE_MODEL_OPT " <variable>:<model>", \
+    "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);

src/util/parse_options.cpp

@@ -9,6 +9,7 @@ Author: Daniel Kroening, [email protected]
 #include "parse_options.h"
 
 #include <algorithm>
+#include <cctype>
 #include <climits>
 #include <iostream>
 
@@ -23,6 +24,7 @@ Author: Daniel Kroening, [email protected]
 #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<decltype(it)>(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;
+}

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

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<std::size_t>(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<decltype(it)>(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::size_t>(std::distance(it_line_begin, right)) >
+          column_width);
+
+  result.append(margin);
+  result.append(it_line_begin, right);
+
+  return result;
+}

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

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 \

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");
+}

unit/util/string_utils/wrap_line.cpp

@@ -0,0 +1,32 @@
+/// Author: Daniel Poetzl
+
+/// \file Tests for wrap_line()
+
+#include <testing-utils/use_catch.h>
+#include <util/string_utils.h>
+
+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");
+  }
+}