Merge pull request #7853 from tautschnig/bugfixes/fix-help-formatting

Fix help formatting errors and omissions

Author: tautschnig

jbmc/src/janalyzer/janalyzer_parse_options.cpp

@@ -794,7 +794,7 @@ void janalyzer_parse_optionst::help()
     "\n"
     "Other options:\n"
     " {y--version} \t show version and exit\n"
-    " {y--verbosity {u#} \t verbosity level\n"
+    " {y--verbosity} {u#} \t verbosity level\n"
     HELP_TIMESTAMP
     "\n");
   // clang-format on

src/analyses/variable-sensitivity/variable_sensitivity_domain.h

@@ -87,7 +87,7 @@
   "value tracking\n"                                                           \
   " {y--vsd-structs} [{ytop-bottom}|{yevery-field}] \t "                       \
   "struct field sensitive analysis\n"                                          \
-  " {y--vsd-arrays} [[ytop-bottom}|{ysmash}|{yup-to-n-elements}|"              \
+  " {y--vsd-arrays} [{ytop-bottom}|{ysmash}|{yup-to-n-elements}|"              \
   "{yevery-element}] \t "                                                      \
   "array entry sensitive analysis\n"                                           \
   " {y--vsd-array-max-elements} {uN} \t "                                      \

src/goto-cc/goto_cc_mode.cpp

@@ -22,6 +22,7 @@ Author: CM Wintersteiger, 2006
 #endif
 
 #include <util/exception_utils.h>
+#include <util/help_formatter.h>
 #include <util/message.h>
 #include <util/parse_options.h>
 #include <util/version.h>
@@ -53,25 +54,28 @@ void goto_cc_modet::help()
             << align_center_with_border("Christoph Wintersteiger") << '\n'
             <<
   "\n";
+  // clang-format on
 
   help_mode();
 
-  std::cout <<
-  "Usage:                       Purpose:\n"
-  "\n"
-  " --verbosity #               verbosity level\n"
-  " --function name             set entry point to name\n"
-  " --native-compiler cmd       command to invoke as preprocessor/compiler\n"
-  " --native-linker cmd         command to invoke as linker\n"
-  " --native-assembler cmd      command to invoke as assembler (goto-as only)\n"
-  " --export-file-local-symbols\n"
-  "                             name-mangle and export file-local symbols\n"
-  " --mangle-suffix suffix      append suffix to exported file-local symbols\n"
-  " --print-rejected-preprocessed-source file\n"
-  "                             copy failing (preprocessed) source to file\n"
-  " --object-bits               number of bits used for object addresses\n"
-  "\n";
-  // clang-format on
+  std::cout << help_formatter(
+    "Usage:                     \tPurpose:\n"
+    "\n"
+    " {y--verbosity} {u#} \t verbosity level\n"
+    " {y--function} {uname} \t set entry point to name\n"
+    " {y--native-compiler} {ucmd} \t command to invoke as "
+    "preprocessor/compiler\n"
+    " {y--native-linker} {ucmd} \t command to invoke as linker\n"
+    " {y--native-assembler} {ucmd} \t command to invoke as assembler "
+    "(goto-as only)\n"
+    " {y--export-file-local-symbols} \t "
+    "name-mangle and export file-local symbols\n"
+    " {y--mangle-suffix} {usuffix} \t append suffix to exported file-local "
+    "symbols\n"
+    " {y--print-rejected-preprocessed-source} {ufile} \t "
+    "copy failing (preprocessed) source to file\n"
+    " {y--object-bits} {N} \t number of bits used for object addresses\n"
+    "\n");
 }
 
 /// starts the compiler

src/goto-checker/bmc_util.h

@@ -227,7 +227,7 @@ void run_property_decider(
   " {y--unwinding-assertions} \t generate unwinding assertions (cannot be "    \
   "used with {y--cover})\n"                                                    \
   " {y--partial-loops} \t permit paths with partial loops\n"                   \
-  " {y--no-self-loops-to-assumptions} \t do not simplify while(1){} to "       \
+  " {y--no-self-loops-to-assumptions} \t do not simplify while(1){ {}} to "    \
   "assume(0)\n"                                                                \
   " {y--symex-complexity-limit} {uN} \t "                                      \
   "how complex ({uN}) a path can become before symex abandons it. Currently "  \

src/goto-instrument/contracts/dynamic-frames/dfcc.h

@@ -55,20 +55,18 @@ class optionst;
 #define FLAG_DFCC "dfcc"
 #define OPT_DFCC "(" FLAG_DFCC "):"
 
-// clang-format off
 #define HELP_DFCC                                                              \
-  " --dfcc <harness>              activate dynamic frame condition checking\n" \
-  "                               for contracts using the given harness as\n"  \
-  "                               entry point\n"
+  " {y--dfcc} {uharness} \t "                                                  \
+  "activate dynamic frame condition checking for contracts using the given "   \
+  "harness as entry point\n"
 
 #define FLAG_ENFORCE_CONTRACT_REC "enforce-contract-rec"
 #define OPT_ENFORCE_CONTRACT_REC "(" FLAG_ENFORCE_CONTRACT_REC "):"
 #define HELP_ENFORCE_CONTRACT_REC                                              \
-  " --enforce-contract-rec <function>[/<contract>]"                            \
-  "                               wrap fun with an assertion of the contract\n"\
-  "                               and assume recursive calls to fun satisfy \n"\
-  "                               the contract\n"
-// clang-format on
+  " {y--enforce-contract-rec} {ufunction}[{y/}{ucontract}] \t "                \
+  "wrap {ufunction} with an assertion of the contract and assume recursive "   \
+  "calls to "                                                                  \
+  "{ufunction} satisfy the contract\n"
 
 /// Exception thrown for bad function/contract specification pairs passed on
 /// the CLI.

src/memory-analyzer/memory_analyzer_parse_options.cpp

@@ -183,8 +183,8 @@ void memory_analyzer_parse_optionst::help()
     "\n"
     "Main options:\n"
     " {y--core-file} {ufile_name} \t analyze from core file {ufile_name}\n"
-    " {y--breakpoint {uname} \t analyze from breakpoint {uname}\n"
-    " {y--symbols {usymbol-list} \t list of symbols to analyze\n"
+    " {y--breakpoint} {uname} \t analyze from breakpoint {uname}\n"
+    " {y--symbols} {usymbol-list} \t list of symbols to analyze\n"
     " {y--symtab-snapshot} \t output snapshot as symbol table\n"
     " {y--output-file} {ufile_name} \t write snapshot to file {ufile_name}\n"
     " {y--json-ui} \t output snapshot in JSON format\n"