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

regression/goto-instrument/uninitialized-check/main.c

@@ -0,0 +1,29 @@
+#include <stdlib.h>
+
+int globals_are_actually_initialized; // See ISO-9899!
+
+int main(int argc, char **argv)
+{
+  int definitely_uninitialized;
+  int maybe_uninitialized;
+  int actually_initialized;
+
+  if(argc > 1)
+  {
+    maybe_uninitialized = 1;
+  }
+
+  if(argc <= 3)
+  {
+    actually_initialized = 0;
+  }
+  if(argc >= 4)
+  {
+    actually_initialized = 1;
+  }
+
+  int *heap_variables_uninitialized = malloc(sizeof(int));
+
+  return definitely_uninitialized + maybe_uninitialized + actually_initialized +
+         globals_are_actually_initialized + *heap_variables_uninitialized;
+}

regression/goto-instrument/uninitialized-check/test.desc

@@ -0,0 +1,16 @@
+CORE
+main.c
+--uninitialized-check
+^\[main.uninitialized_local.1\] line \d+ use of uninitialized local variable main::1::definitely_uninitialized: FAILURE$
+^\[main.uninitialized_local.2\] line \d+ use of uninitialized local variable main::1::maybe_uninitialized: FAILURE$
+^\[main.uninitialized_local.3\] line \d+ use of uninitialized local variable main::1::actually_initialized: SUCCESS$
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+A basic test of the uninitialized variable check.
+In an ideal world there would be a check for heap_variables_uninitialized
+that would fail however this is beyond the current scope of the analysis.
+

src/goto-diff/goto_diff_parse_options.cpp

@@ -70,9 +70,6 @@ void goto_diff_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("cover"))
     parse_cover_options(cmdline, options);
 
-  if(cmdline.isset("mm"))
-    options.set_option("mm", cmdline.get_value("mm"));
-
   // all checks supported by goto_check
   PARSE_OPTIONS_GOTO_CHECK(cmdline, options);
 

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"
@@ -110,11 +107,9 @@ Author: Daniel Kroening, [email protected]
 #include "stack_depth.h"
 #include "thread_instrumentation.h"
 #include "undefined_functions.h"
-#include "uninitialized.h"
 #include "unwind.h"
 #include "unwindset.h"
 #include "value_set_fi_fp_removal.h"
-#include "wmm/weak_memory.h"
 
 /// invoke main modules
 int goto_instrument_parse_optionst::doit()
@@ -1722,14 +1717,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
@@ -1762,7 +1756,7 @@ void goto_instrument_parse_optionst::help()
     "Safety checks:\n"
     " --no-assertions              ignore user assertions\n"
     HELP_GOTO_CHECK
-    " --uninitialized-check        add checks for uninitialized locals (experimental)\n" // NOLINT(*)
+    HELP_UNINITIALIZED_CHECK
     " --stack-depth n              add check that call stack size of non-inlined functions never exceeds n\n" // NOLINT(*)
     " --race-check                 add floating-point data race checks\n"
     "\n"
@@ -1780,7 +1774,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)
@@ -1798,17 +1792,7 @@ void goto_instrument_parse_optionst::help()
     " --skip-loops <loop-ids>      add gotos to skip selected loops during execution\n" // NOLINT(*)
     "\n"
     "Memory model instrumentations:\n"
-    " --mm <tso,pso,rmo,power>     instruments a weak memory model\n"
-    " --scc                        detects critical cycles per SCC (one thread per SCC)\n" // NOLINT(*)
-    " --one-event-per-cycle        only instruments one event per cycle\n"
-    " --minimum-interference       instruments an optimal number of events\n"
-    " --my-events                  only instruments events whose ids appear in inst.evt\n" // NOLINT(*)
-    " --cfg-kill                   enables symbolic execution used to reduce spurious cycles\n" // NOLINT(*)
-    " --no-dependencies            no dependency analysis\n"
-    // NOLINTNEXTLINE(whitespace/line_length)
-    " --no-po-rendering            no representation of the threads in the dot\n"
-    " --render-cluster-file        clusterises the dot by files\n"
-    " --render-cluster-function    clusterises the dot by functions\n"
+    HELP_WMM_FULL
     "\n"
     "Slicing:\n"
     HELP_REACHABILITY_SLICER
@@ -1853,11 +1837,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,42 +28,37 @@ 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 "count_eloc.h"
+#include "document_properties.h"
+#include "dump_c.h"
 #include "generate_function_bodies.h"
 #include "insert_final_assert_false.h"
 #include "nondet_volatile.h"
 #include "replace_calls.h"
-
-#include "count_eloc.h"
+#include "uninitialized.h"
+#include "wmm/weak_memory.h"
 
 // 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)" \
-  "(minimum-interference)" \
-  "(mm):(my-events)" \
+  OPT_UNINITIALIZED_CHECK \
+  OPT_WMM \
+  "(race-check)" \
   "(unwind):(unwindset):(unwindset-file):" \
   "(unwinding-assertions)(partial-loops)(continue-as-loops)" \
   "(log):" \
-  "(max-var):(max-po-trans):(ignore-arrays)" \
-  "(cfg-kill)(no-dependencies)(force-loop-duplication)" \
   "(call-graph)(reachable-call-graph)" \
   OPT_INSERT_FINAL_ASSERT_FALSE \
   OPT_SHOW_CLASS_HIERARCHY \
-  "(no-po-rendering)(render-cluster-file)(render-cluster-function)" \
   "(isr):" \
   "(stack-depth):(nondet-static)" \
   "(nondet-static-exclude):" \
@@ -87,7 +82,6 @@ Author: Daniel Kroening, [email protected]
   "(remove-function-pointers)" \
   "(show-claims)(property):" \
   "(show-symbol-table)(show-points-to)(show-rw-set)" \
-  "(cav11)" \
   OPT_TIMESTAMP \
   "(show-natural-loops)(show-lexical-loops)(accelerate)(havoc-loops)" \
   "(string-abstraction)" \

src/goto-instrument/uninitialized.cpp

@@ -158,7 +158,7 @@ void uninitializedt::add_assertions(
                 symbol_exprt(new_identifier, bool_typet()),
                 instruction.source_location());
             assertion.source_location_nonconst().set_comment(
-              "use of uninitialized local variable");
+              "use of uninitialized local variable " + id2string(identifier));
             assertion.source_location_nonconst().set_property_class(
               "uninitialized local");
 

src/goto-instrument/uninitialized.h

@@ -24,4 +24,10 @@ void show_uninitialized(
   const goto_modelt &,
   std::ostream &out);
 
+#define OPT_UNINITIALIZED_CHECK "(uninitialized-check)"
+
+#define HELP_UNINITIALIZED_CHECK                                               \
+  " --uninitialized-check        add checks for uninitialized locals "         \
+  "(experimental)\n" // NOLINT(whitespace/line_length)
+
 #endif // CPROVER_GOTO_INSTRUMENT_UNINITIALIZED_H

src/goto-instrument/wmm/weak_memory.h

@@ -54,4 +54,55 @@ void introduce_temporaries(
 #endif
   messaget &message);
 
+// clang-format off
+#define OPT_WMM_MEMORY_MODEL  "(mm):"
+
+#define OPT_WMM_INSTRUMENTATION_STRATEGIES                                     \
+  "(one-event-per-cycle)"                                                      \
+  "(minimum-interference)"                                                     \
+  "(read-first)"                                                               \
+  "(write-first)"                                                              \
+  "(my-events)"                                                                \
+
+#define OPT_WMM_LIMITS                                                         \
+  "(max-var):"                                                                 \
+  "(max-po-trans):"                                                            \
+
+#define OPT_WMM_LOOPS                                                          \
+  "(force-loop-duplication)"                                                   \
+  "(no-loop-duplication)"                                                      \
+
+#define OPT_WMM_MISC                                                           \
+  "(scc)"                                                                      \
+  "(cfg-kill)"                                                                 \
+  "(no-dependencies)"                                                          \
+  "(no-po-rendering)"                                                          \
+  "(render-cluster-file)"                                                      \
+  "(render-cluster-function)"                                                  \
+  "(cav11)"                                                                    \
+  "(hide-internals)"                                                           \
+  "(ignore-arrays)"                                                            \
+
+#define OPT_WMM                                                                \
+  OPT_WMM_MEMORY_MODEL                                                         \
+  OPT_WMM_INSTRUMENTATION_STRATEGIES                                           \
+  OPT_WMM_LIMITS                                                               \
+  OPT_WMM_LOOPS                                                                \
+  OPT_WMM_MISC                                                                 \
+
+
+#define HELP_WMM_FULL                                                          \
+  " --mm <tso,pso,rmo,power>     instruments a weak memory model\n"            \
+  " --scc                        detects critical cycles per SCC (one thread per SCC)\n" /* NOLINT(whitespace/line_length) */ \
+  " --one-event-per-cycle        only instruments one event per cycle\n"       \
+  " --minimum-interference       instruments an optimal number of events\n"    \
+  " --my-events                  only instruments events whose ids appear in inst.evt\n" /* NOLINT(whitespace/line_length) */ \
+  " --cfg-kill                   enables symbolic execution used to reduce spurious cycles\n" /* NOLINT(whitespace/line_length) */ \
+  " --no-dependencies            no dependency analysis\n"                     \
+  " --no-po-rendering            no representation of the threads in the dot\n"\
+  " --render-cluster-file        clusterises the dot by files\n"               \
+  " --render-cluster-function    clusterises the dot by functions\n"
+
+// clang-format on
+
 #endif // CPROVER_GOTO_INSTRUMENT_WMM_WEAK_MEMORY_H