Regroup goto-instrument's options in help output

Some options were placed under a heading that wasn't applicable to them.
Instead, this commit tries to come up with groups that may allow a user
to find what they are looking for.

No changes to the total set of documented options other than adding
"--verbosity."

Author: tautschnig

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1748,43 +1748,42 @@ void goto_instrument_parse_optionst::help()
     "Usage:                       Purpose:\n"
     "\n"
     " goto-instrument [-?] [-h] [--help]  show help\n"
-    " goto-instrument in out              perform instrumentation\n"
-    "\n"
-    "Main options:\n"
-    HELP_DOCUMENT_PROPERTIES
-    " --dot                        generate CFG graph in DOT format\n"
-    " --interpreter                do concrete execution\n"
+    " goto-instrument --version           show version and exit\n"
+    " goto-instrument [options] in [out]  perform analysis or instrumentation\n"
     "\n"
     "Dump Source:\n"
     HELP_DUMP_C
     "\n"
     "Diagnosis:\n"
     HELP_SHOW_PROPERTIES
+    HELP_DOCUMENT_PROPERTIES
     " --show-symbol-table          show loaded symbol table\n"
     " --list-symbols               list symbols with type information\n"
     HELP_SHOW_GOTO_FUNCTIONS
     HELP_GOTO_PROGRAM_STATS
-    " --drop-unused-functions      drop functions trivially unreachable from main function\n" // NOLINT(*)
+    " --dot                        generate CFG graph in DOT format\n"
     " --print-internal-representation\n" // NOLINTNEXTLINE(*)
     "                              show verbose internal representation of the program\n"
     " --list-undefined-functions   list functions without body\n"
-    " --show-struct-alignment      show struct members that might be concurrently accessed\n" // NOLINT(*)
-    " --show-natural-loops         show natural loop heads\n"
     // NOLINTNEXTLINE(whitespace/line_length)
     " --list-calls-args            list all function calls with their arguments\n"
     " --call-graph                 show graph of function calls\n"
     // NOLINTNEXTLINE(whitespace/line_length)
     " --reachable-call-graph       show graph of function calls potentially reachable from main function\n"
     HELP_SHOW_CLASS_HIERARCHY
+    HELP_VALIDATE
+    // NOLINTNEXTLINE(whitespace/line_length)
+    " --validate-goto-binary       check the well-formedness of the passed in goto\n"
+    "                              binary and then exit\n"
+    " --interpreter                do concrete execution\n"
+    "\n"
+    "Data-flow analyses:\n"
+    " --show-struct-alignment      show struct members that might be concurrently accessed\n" // NOLINT(*)
     // NOLINTNEXTLINE(whitespace/line_length)
     " --show-threaded              show instructions that may be executed by more than one thread\n"
     " --show-local-safe-pointers   show pointer expressions that are trivially dominated by a not-null check\n" // NOLINT(*)
     " --show-safe-dereferences     show pointer expressions that are trivially dominated by a not-null check\n" // NOLINT(*)
     "                              *and* used as a dereference operand\n" // NOLINT(*)
-    HELP_VALIDATE
-    // NOLINTNEXTLINE(whitespace/line_length)
-    " --validate-goto-binary       check the well-formedness of the passed in goto\n"
-    "                              binary and then exit\n"
     "\n"
     "Safety checks:\n"
     " --no-assertions              ignore user assertions\n"
@@ -1795,33 +1794,56 @@ void goto_instrument_parse_optionst::help()
     "\n"
     "Semantic transformations:\n"
     << HELP_NONDET_VOLATILE <<
-    HELP_UNWINDSET
-    " --unwindset-file <file>      read unwindset from file\n"
-    " --partial-loops              permit paths with partial loops\n"
-    " --unwinding-assertions       generate unwinding assertions\n"
-    " --continue-as-loops          add loop for remaining iterations after unwound part\n" // NOLINT(*)
     " --isr <function>             instruments an interrupt service routine\n"
     " --mmio                       instruments memory-mapped I/O\n"
     " --nondet-static              add nondeterministic initialization of variables with static lifetime\n" // NOLINT(*)
     " --nondet-static-exclude e    same as nondet-static except for the variable e\n" //NOLINT(*)
     "                              (use multiple times if required)\n"
     " --check-invariant function   instruments invariant checking function\n"
-    HELP_REMOVE_POINTERS
     " --splice-call caller,callee  prepends a call to callee in the body of caller\n"  // NOLINT(*)
     " --undefined-function-is-assume-false\n"
     // NOLINTNEXTLINE(whitespace/line_length)
     "                              convert each call to an undefined function to assume(false)\n"
     HELP_INSERT_FINAL_ASSERT_FALSE
     HELP_REPLACE_FUNCTION_BODY
+    HELP_RESTRICT_FUNCTION_POINTER
+    HELP_REMOVE_CALLS_NO_BODY
+    " --add-library                add models of C library functions\n"
+    HELP_CONFIG_LIBRARY
+    " --model-argc-argv <n>        model up to <n> command line arguments\n"
+    // NOLINTNEXTLINE(whitespace/line_length)
+    " --remove-function-body <f>   remove the implementation of function <f> (may be repeated)\n"
+    HELP_REPLACE_CALLS
     HELP_ANSI_C_LANGUAGE
     "\n"
-    "Loop transformations:\n"
+    "Semantics-preserving transformations:\n"
+    " --drop-unused-functions      drop functions trivially unreachable from main function\n" // NOLINT(*)
+    HELP_REMOVE_POINTERS
+    " --constant-propagator        propagate constants and simplify expressions\n" // NOLINT(*)
+    " --inline                     perform full inlining\n"
+    " --partial-inline             perform partial inlining\n"
+    " --function-inline <function> transitively inline all calls <function> makes\n" // NOLINT(*)
+    " --no-caching                 disable caching of intermediate results during transitive function inlining\n" // NOLINT(*)
+    " --log <file>                 log in json format which code segments were inlined, use with --function-inline\n" // NOLINT(*)
+    " --remove-function-pointers   replace function pointers by case statement over function calls\n" // NOLINT(*)
+    HELP_REMOVE_CONST_FUNCTION_POINTERS
+    " --value-set-fi-fp-removal    build flow-insensitive value set and replace function pointers by a case statement\n" // NOLINT(*)
+    "                              over the possible assignments. If the set of possible assignments is empty the function pointer\n" // NOLINT(*)
+    "                              is removed using the standard remove-function-pointers pass. \n" // NOLINT(*)
+    "\n"
+    "Loop information and transformations:\n"
+    HELP_UNWINDSET
+    " --unwindset-file <file>      read unwindset from file\n"
+    " --partial-loops              permit paths with partial loops\n"
+    " --unwinding-assertions       generate unwinding assertions\n"
+    " --continue-as-loops          add loop for remaining iterations after unwound part\n" // NOLINT(*)
     " --k-induction <k>            check loops with k-induction\n"
     " --step-case                  k-induction: do step-case\n"
     " --base-case                  k-induction: do base-case\n"
     " --havoc-loops                over-approximate all loops\n"
     " --accelerate                 add loop accelerators\n"
     " --skip-loops <loop-ids>      add gotos to skip selected loops during execution\n" // NOLINT(*)
+    " --show-natural-loops         show natural loop heads\n"
     "\n"
     "Memory model instrumentations:\n"
     HELP_WMM_FULL
@@ -1840,41 +1862,20 @@ void goto_instrument_parse_optionst::help()
     "                             force the aggressive slicer to preserve function <f>\n" // NOLINT(*)
     " --aggressive-slice-preserve-function containing <f>\n"
     "                              force the aggressive slicer to preserve all functions with names containing <f>\n" // NOLINT(*)
-    "--aggressive-slice-preserve-all-direct-paths \n"
+    " --aggressive-slice-preserve-all-direct-paths \n"
     "                             force aggressive slicer to preserve all direct paths\n" // NOLINT(*)
     "\n"
-    "Further transformations:\n"
-    " --constant-propagator        propagate constants and simplify expressions\n" // NOLINT(*)
-    " --inline                     perform full inlining\n"
-    " --partial-inline             perform partial inlining\n"
-    " --function-inline <function> transitively inline all calls <function> makes\n" // NOLINT(*)
-    " --no-caching                 disable caching of intermediate results during transitive function inlining\n" // NOLINT(*)
-    " --log <file>                 log in json format which code segments were inlined, use with --function-inline\n" // NOLINT(*)
-    " --remove-function-pointers   replace function pointers by case statement over function calls\n" // NOLINT(*)
-    " --value-set-fi-fp-removal    build flow-insensitive value set and replace function pointers by a case statement\n" // NOLINT(*)
-    "                              over the possible assignments. If the set of possible assignments is empty the function pointer\n" // NOLINT(*)
-    "                              is removed using the standard remove-function-pointers pass. \n" // NOLINT(*)
-    HELP_RESTRICT_FUNCTION_POINTER
-    HELP_REMOVE_CALLS_NO_BODY
-    HELP_REMOVE_CONST_FUNCTION_POINTERS
-    " --add-library                add models of C library functions\n"
-    HELP_CONFIG_LIBRARY
-    " --model-argc-argv <n>        model up to <n> command line arguments\n"
-    // NOLINTNEXTLINE(whitespace/line_length)
-    " --remove-function-body <f>   remove the implementation of function <f> (may be repeated)\n"
-    HELP_REPLACE_CALLS
-    "\n"
     "Code contracts:\n"
     HELP_LOOP_CONTRACTS
     HELP_REPLACE_CALL
     HELP_ENFORCE_CONTRACT
     "\n"
-    "Other options:\n"
-    " --version                    show version and exit\n"
+    "User-interface options:\n"
     HELP_FLUSH
     " --xml                        output files in XML where supported\n"
     " --xml-ui                     use XML-formatted output\n"
     " --json-ui                    use JSON-formatted output\n"
+    " --verbosity #                verbosity level\n"
     HELP_TIMESTAMP
     "\n";
   // clang-format on