Extract constants for --cover help message and options

These were previously duplicated between 3 different executables.

Author: hannes-steffenhagen-diffblue

jbmc/src/jdiff/jdiff_parse_options.cpp

@@ -367,7 +367,7 @@ void jdiff_parse_optionst::help()
     "\n"
     "Program instrumentation options:\n"
     HELP_GOTO_CHECK
-    " --cover CC                   create test-suite with coverage criterion CC\n" // NOLINT(*)
+    HELP_COVER
     "Java Bytecode frontend options:\n"
     JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP
     "Other options:\n"

jbmc/src/jdiff/jdiff_parse_options.h

@@ -23,6 +23,8 @@ Author: Peter Schrammel
 #include <goto-programs/show_goto_functions.h>
 #include <goto-programs/show_properties.h>
 
+#include <goto-instrument/cover.h>
+
 class goto_modelt;
 
 // clang-format off
@@ -31,7 +33,7 @@ class goto_modelt;
   OPT_SHOW_GOTO_FUNCTIONS \
   OPT_SHOW_PROPERTIES \
   OPT_GOTO_CHECK \
-  "(cover):" \
+  OPT_COVER \
   "(verbosity):(version)" \
   "(no-lazy-methods)" /* should go away */ \
   "(no-refine-strings)" /* should go away */ \

src/cbmc/cbmc_parse_options.cpp

@@ -1118,7 +1118,7 @@ void cbmc_parse_optionst::help()
     " --no-assertions              ignore user assertions\n"
     " --no-assumptions             ignore user assumptions\n"
     " --error-label label          check that label is unreachable\n"
-    " --cover CC                   create test-suite with coverage criterion CC\n" // NOLINT(*)
+    HELP_COVER
     " --mm MM                      memory consistency model for concurrent programs\n" // NOLINT(*)
     // NOLINTNEXTLINE(whitespace/line_length)
     " --malloc-fail-assert         set malloc failure mode to assert-then-assume\n"

src/cbmc/cbmc_parse_options.h

@@ -34,6 +34,8 @@ Author: Daniel Kroening, [email protected]
 #include <json/json_interface.h>
 #include <xmllang/xml_interface.h>
 
+#include <goto-instrument/cover.h>
+
 class goto_functionst;
 class optionst;
 
@@ -73,8 +75,9 @@ class optionst;
   "(property):(stop-on-fail)(trace)" \
   "(error-label):(verbosity):(no-library)" \
   "(nondet-static)" \
-  "(version)" \
-  "(cover):(symex-coverage-report):" \
+  "(version)"        \
+  OPT_COVER \
+  "(symex-coverage-report):" \
   "(mm):" \
   OPT_TIMESTAMP \
   "(i386-linux)(i386-macos)(i386-win32)(win32)(winx64)(gcc)" \

src/goto-diff/goto_diff_parse_options.cpp

@@ -411,7 +411,7 @@ void goto_diff_parse_optionst::help()
     "\n"
     "Program instrumentation options:\n"
     HELP_GOTO_CHECK
-    " --cover CC                   create test-suite with coverage criterion CC\n" // NOLINT(*)
+    HELP_COVER
     "Other options:\n"
     " --version                    show version and exit\n"
     " --json-ui                    use JSON-formatted output\n"

src/goto-diff/goto_diff_parse_options.h

@@ -22,6 +22,8 @@ Author: Peter Schrammel
 #include <goto-programs/show_goto_functions.h>
 #include <goto-programs/show_properties.h>
 
+#include <goto-instrument/cover.h>
+
 class goto_modelt;
 class optionst;
 
@@ -31,7 +33,7 @@ class optionst;
   OPT_SHOW_GOTO_FUNCTIONS \
   OPT_SHOW_PROPERTIES \
   OPT_GOTO_CHECK \
-  "(cover):" \
+  OPT_COVER \
   "(verbosity):(version)" \
   OPT_FLUSH \
   OPT_TIMESTAMP \

src/goto-instrument/cover.h

@@ -22,6 +22,10 @@ class message_handlert;
 class cmdlinet;
 class optionst;
 
+#define OPT_COVER "(cover):"
+#define HELP_COVER \
+  " --cover CC                   create test-suite with coverage criterion CC\n"
+
 enum class coverage_criteriont
 {
   LOCATION,