Tidying up the options for goto-instrument

regression/cbmc-cpp/Overloading_Operators16/test.desc

@@ -1,6 +1,6 @@
 KNOWNBUG
 main.cpp
---no-pointer-check
+
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-cpp/virtual11/test.desc

@@ -1,6 +1,6 @@
 KNOWNBUG
 main.cpp
---unwind 1 --no-pointer-check
+--unwind 1
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-cpp/virtual12/test.desc

@@ -1,6 +1,6 @@
 KNOWNBUG
 main.cpp
---unwind 1 --no-pointer-check
+--unwind 1
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/cbmc-cpp/virtual3/test.desc

@@ -1,6 +1,6 @@
 KNOWNBUG
 main.cpp
---no-pointer-check
+
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

regression/goto-instrument/document-properties-basic/html.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--document-properties-html
+^EXIT=0$
+^SIGNAL=0$
+^<em>  assert\(1 == 1\);<\/em>$
+--
+^warning: ignoring
+--
+Tests whether this option works at all.

regression/goto-instrument/document-properties-basic/latex.desc

@@ -0,0 +1,10 @@
+CORE
+main.c
+--document-properties-latex
+^EXIT=0$
+^SIGNAL=0$
+^\\claim\{assertion 1 == 1\}$
+--
+^warning: ignoring
+--
+Tests whether this option works at all.

regression/goto-instrument/document-properties-basic/main.c

@@ -0,0 +1,8 @@
+#include <assert.h>
+
+int main(int argc, char **argv)
+{
+  assert(1 == 1);
+
+  return 0;
+}

src/goto-instrument/document_properties.h

@@ -24,4 +24,15 @@ void document_properties_html(
   const goto_modelt &,
   std::ostream &out);
 
+#define OPT_DOCUMENT_PROPERTIES                                                \
+  "(document-claims-latex)(document-claims-html)"                              \
+  "(document-properties-latex)(document-properties-html)"
+
+// clang-format off
+#define HELP_DOCUMENT_PROPERTIES                                               \
+  " --document-properties-html   generate HTML property documentation\n"       \
+  " --document-properties-latex  generate Latex property documentation\n"
+
+// clang-format on
+
 #endif // CPROVER_GOTO_INSTRUMENT_DOCUMENT_PROPERTIES_H

src/goto-instrument/dump_c.h

@@ -43,4 +43,20 @@ void dump_cpp(
   const namespacet &ns,
   std::ostream &out);
 
+#define OPT_DUMP_C                                                             \
+  "(dump-c)(dump-cpp)"                                                         \
+  "(dump-c-type-header):"                                                      \
+  "(no-system-headers)(use-all-headers)(harness)"
+
+// clang-format off
+#define HELP_DUMP_C                                                            \
+    " --dump-c                     generate C source\n"                        \
+    " --dump-c-type-header m       generate a C header for types local in m\n" \
+    " --dump-cpp                   generate C++ source\n"                      \
+    " --no-system-headers          generate C source expanding libc includes\n"\
+    " --use-all-headers            generate C source with all includes\n"      \
+    " --harness                    include input generator in output\n"
+
+// clang-format on
+
 #endif // CPROVER_GOTO_INSTRUMENT_DUMP_C_H

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -52,7 +52,6 @@ Author: Daniel Kroening, [email protected]
 #include <goto-programs/write_goto_binary.h>
 
 #include <pointer-analysis/add_failed_symbols.h>
-#include <pointer-analysis/goto_program_dereference.h>
 #include <pointer-analysis/show_value_sets.h>
 #include <pointer-analysis/value_set_analysis.h>
 
@@ -85,9 +84,7 @@ Author: Daniel Kroening, [email protected]
 #include "branch.h"
 #include "call_sequences.h"
 #include "concurrency.h"
-#include "document_properties.h"
 #include "dot.h"
-#include "dump_c.h"
 #include "full_slicer.h"
 #include "function.h"
 #include "havoc_loops.h"
@@ -1722,14 +1719,13 @@ void goto_instrument_parse_optionst::help()
     " goto-instrument in out              perform instrumentation\n"
     "\n"
     "Main options:\n"
-    " --document-properties-html   generate HTML property documentation\n"
-    " --document-properties-latex  generate Latex property documentation\n"
-    " --dump-c                     generate C source\n"
-    " --dump-c-type-header m       generate a C header for types local in m\n"
-    " --dump-cpp                   generate C++ source\n"
+    HELP_DOCUMENT_PROPERTIES
     " --dot                        generate CFG graph in DOT format\n"
     " --interpreter                do concrete execution\n"
     "\n"
+    "Dump Source:\n"
+    HELP_DUMP_C
+    "\n"
     "Diagnosis:\n"
     " --show-loops                 show the loops in the program\n"
     HELP_SHOW_PROPERTIES
@@ -1780,7 +1776,7 @@ void goto_instrument_parse_optionst::help()
     " --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"
-    " --remove-pointers            converts pointer arithmetic to base+offset expressions\n" // NOLINT(*)
+    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)
@@ -1853,11 +1849,9 @@ void goto_instrument_parse_optionst::help()
     HELP_ENFORCE_CONTRACT
     "\n"
     "Other options:\n"
-    " --no-system-headers          with --dump-c/--dump-cpp: generate C source expanding libc includes\n" // NOLINT(*)
-    " --use-all-headers            with --dump-c/--dump-cpp: generate C source with all includes\n" // NOLINT(*)
-    " --harness                    with --dump-c/--dump-cpp: include input generator in output\n" // NOLINT(*)
     " --version                    show version and exit\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"
     HELP_TIMESTAMP

src/goto-instrument/goto_instrument_parse_options.h

@@ -28,8 +28,12 @@ Author: Daniel Kroening, [email protected]
 
 #include <analyses/goto_check.h>
 
+#include <pointer-analysis/goto_program_dereference.h>
+
 #include "aggressive_slicer.h"
 #include "contracts/contracts.h"
+#include "document_properties.h"
+#include "dump_c.h"
 #include "generate_function_bodies.h"
 #include "insert_final_assert_false.h"
 #include "nondet_volatile.h"
@@ -39,17 +43,11 @@ Author: Daniel Kroening, [email protected]
 
 // clang-format off
 #define GOTO_INSTRUMENT_OPTIONS \
-  "(all)" \
-  "(document-claims-latex)(document-claims-html)" \
-  "(document-properties-latex)(document-properties-html)" \
-  "(dump-c-type-header):" \
-  "(dump-c)(dump-cpp)(no-system-headers)(use-all-headers)(dot)(xml)" \
-  "(harness)" \
+  OPT_DOCUMENT_PROPERTIES \
+  OPT_DUMP_C \
+  "(dot)(xml)" \
   OPT_GOTO_CHECK \
-  /* no-X-check are deprecated and ignored */ \
-  "(no-bounds-check)(no-pointer-check)(no-div-by-zero-check)" \
-  "(no-nan-check)" \
-  "(remove-pointers)" \
+  OPT_REMOVE_POINTERS \
   "(no-simplify)" \
   "(uninitialized-check)" \
   "(race-check)(scc)(one-event-per-cycle)" \

src/pointer-analysis/goto_program_dereference.h

@@ -107,4 +107,12 @@ void remove_pointers(
   goto_modelt &,
   value_setst &);
 
+#define OPT_REMOVE_POINTERS "(remove-pointers)"
+
+// clang-format off
+#define HELP_REMOVE_POINTERS                                                   \
+  " --remove-pointers            converts pointer arithmetic to base+offset expressions\n" /* NOLINT(whitespace/line_length) */
+
+// clang-format on
+
 #endif // CPROVER_POINTER_ANALYSIS_GOTO_PROGRAM_DEREFERENCE_H