Factor out show properties command line def and docs

to avoid repetition across the CPROVER tools

Author: peterschrammel

src/cbmc/cbmc_parse_options.cpp

@@ -924,7 +924,7 @@ void cbmc_parse_optionst::help()
     " cbmc file.c ...              source file names\n"
     "\n"
     "Analysis options:\n"
-    " --show-properties            show the properties, but don't run analysis\n" // NOLINT(*)
+    HELP_SHOW_PROPERTIES
     " --symex-coverage-report f    generate a Cobertura XML coverage report in f\n" // NOLINT(*)
     " --property id                only check one specific property\n"
     " --stop-on-fail               stop analysis once a failed property is detected\n" // NOLINT(*)

src/cbmc/cbmc_parse_options.h

@@ -53,9 +53,9 @@ class optionst;
   "(aig)(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
   "(little-endian)(big-endian)" \
   OPT_SHOW_GOTO_FUNCTIONS \
+  OPT_SHOW_PROPERTIES \
   "(show-loops)" \
   "(show-symbol-table)(show-parse-tree)(show-vcc)" \
-  "(show-claims)(claim):(show-properties)" \
   "(drop-unused-functions)" \
   "(property):(stop-on-fail)(trace)" \
   "(error-label):(verbosity):(no-library)" \
@@ -72,7 +72,7 @@ class optionst;
   "(graphml-witness):" \
   "(localize-faults)(localize-faults-method):" \
   OPT_GOTO_TRACE \
-  "(fixedbv)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)
+  "(claim):(show-claims)(fixedbv)(floatbv)(all-claims)(all-properties)" // legacy, and will eventually disappear // NOLINT(whitespace/line_length)
 // clang-format on
 
 class cbmc_parse_optionst:

src/clobber/clobber_parse_options.h

@@ -19,23 +19,27 @@ Author: Daniel Kroening, [email protected]
 
 #include <analyses/goto_check.h>
 #include <goto-programs/show_goto_functions.h>
+#include <goto-programs/show_properties.h>
 
 #include <java_bytecode/java_bytecode_language.h>
 
 class goto_functionst;
 class optionst;
 
+// clang-format off
 #define CLOBBER_OPTIONS \
   "(depth):(context-bound):(unwind):" \
   OPT_GOTO_CHECK \
   OPT_SHOW_GOTO_FUNCTIONS \
+  OPT_SHOW_PROPERTIES \
   "(no-assertions)(no-assumptions)" \
   "(error-label):(verbosity):(no-library)" \
   "(version)" \
   "(string-abstraction)" \
-  "(show-locs)(show-vcc)(show-properties)(show-trace)" \
+  "(show-locs)(show-vcc)(show-trace)" \
   "(property):" \
   JAVA_BYTECODE_LANGUAGE_OPTIONS
+// clang-format on
 
 class clobber_parse_optionst:
   public parse_options_baset,

src/goto-analyzer/goto_analyzer_parse_options.cpp

@@ -815,6 +815,7 @@ void goto_analyzer_parse_optionst::help()
 
   std::cout << " * *\n";
 
+  // clang-format off
   std::cout <<
     "* *                Daniel Kroening, DiffBlue                * *\n"
     "* *                 [email protected]                   * *\n"
@@ -898,8 +899,7 @@ void goto_analyzer_parse_optionst::help()
     " --show-parse-tree            show parse tree\n"
     " --show-symbol-table          show symbol table\n"
     HELP_SHOW_GOTO_FUNCTIONS
-    // NOLINTNEXTLINE(whitespace/line_length)
-    " --show-properties            show the properties, but don't run analysis\n"
+    HELP_SHOW_PROPERTIES
     "\n"
     "Program instrumentation options:\n"
     HELP_GOTO_CHECK
@@ -908,4 +908,5 @@ void goto_analyzer_parse_optionst::help()
     " --version                    show version and exit\n"
     HELP_TIMESTAMP
     "\n";
+  // clang-format on
 }

src/goto-analyzer/goto_analyzer_parse_options.h

@@ -109,6 +109,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <goto-programs/goto_model.h>
 #include <goto-programs/show_goto_functions.h>
+#include <goto-programs/show_properties.h>
 
 #include <analyses/ai.h>
 #include <analyses/goto_check.h>
@@ -119,17 +120,19 @@ class bmct;
 class goto_functionst;
 class optionst;
 
+// clang-format off
 #define GOTO_ANALYSER_OPTIONS \
   OPT_FUNCTIONS \
   "D:I:(std89)(std99)(std11)" \
   "(classpath):(cp):(main-class):" \
   "(16)(32)(64)(LP64)(ILP64)(LLP64)(ILP32)(LP32)" \
   "(little-endian)(big-endian)" \
   OPT_SHOW_GOTO_FUNCTIONS \
+  OPT_SHOW_PROPERTIES \
   OPT_GOTO_CHECK \
   "(show-loops)" \
   "(show-symbol-table)(show-parse-tree)" \
-  "(show-properties)(show-reachable-properties)(property):" \
+  "(show-reachable-properties)(property):" \
   "(verbosity):(version)" \
   "(gcc)(arch):" \
   "(taint):(show-taint)" \
@@ -147,6 +150,7 @@ class optionst;
   "(location-sensitive)(concurrent)" \
   "(no-simplify-slicing)" \
   JAVA_BYTECODE_LANGUAGE_OPTIONS
+// clang-format on
 
 class goto_analyzer_parse_optionst:
   public parse_options_baset,

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1452,6 +1452,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
 /// display command line help
 void goto_instrument_parse_optionst::help()
 {
+  // clang-format off
   std::cout <<
     "\n"
     "* *     Goto-Instrument " CBMC_VERSION " - Copyright (C) 2008-2013       * *\n" // NOLINT(*)
@@ -1475,7 +1476,7 @@ void goto_instrument_parse_optionst::help()
     "\n"
     "Diagnosis:\n"
     " --show-loops                 show the loops in the program\n"
-    " --show-properties            show the properties\n"
+    HELP_SHOW_PROPERTIES
     " --show-symbol-table          show symbol table\n"
     " --list-symbols               list symbols with type information\n"
     HELP_SHOW_GOTO_FUNCTIONS
@@ -1570,4 +1571,5 @@ void goto_instrument_parse_optionst::help()
     " --json-ui                    use JSON-formatted output\n"
     HELP_TIMESTAMP
     "\n";
+  // clang-format on
 }

src/goto-instrument/goto_instrument_parse_options.h

@@ -18,10 +18,12 @@ Author: Daniel Kroening, [email protected]
 
 #include <goto-programs/goto_functions.h>
 #include <goto-programs/show_goto_functions.h>
+#include <goto-programs/show_properties.h>
 #include <goto-programs/remove_const_function_pointers.h>
 
 #include <analyses/goto_check.h>
 
+// clang-format off
 #define GOTO_INSTRUMENT_OPTIONS \
   "(all)" \
   "(document-claims-latex)(document-claims-html)" \
@@ -51,6 +53,7 @@ Author: Daniel Kroening, [email protected]
   "(stack-depth):(nondet-static)" \
   "(function-enter):(function-exit):(branch):" \
   OPT_SHOW_GOTO_FUNCTIONS \
+  OPT_SHOW_PROPERTIES \
   "(drop-unused-functions)" \
   "(show-value-sets)" \
   "(show-global-may-alias)" \
@@ -64,7 +67,7 @@ Author: Daniel Kroening, [email protected]
   OPT_REMOVE_CONST_FUNCTION_POINTERS \
   "(print-internal-representation)" \
   "(remove-function-pointers)" \
-  "(show-claims)(show-properties)(property):" \
+  "(show-claims)(property):" \
   "(show-symbol-table)(show-points-to)(show-rw-set)" \
   "(cav11)" \
   OPT_TIMESTAMP \
@@ -81,8 +84,8 @@ Author: Daniel Kroening, [email protected]
   "(show-threaded)(list-calls-args)(print-path-lengths)" \
   "(undefined-function-is-assume-false)" \
   "(remove-function-body):"\
-  "(splice-call):" \
-
+  "(splice-call):"
+// clang-format on
 
 class goto_instrument_parse_optionst:
   public parse_options_baset,

src/goto-programs/show_properties.h

@@ -22,6 +22,14 @@ class goto_programt;
 class goto_functionst;
 class message_handlert;
 
+// clang-format off
+#define OPT_SHOW_PROPERTIES \
+  "(show-properties)"
+
+#define HELP_SHOW_PROPERTIES \
+  " --show-properties            show the properties, but don't run analysis\n" // NOLINT(*)
+// clang-format on
+
 void show_properties(
   const goto_modelt &,
   message_handlert &message_handler,

src/jbmc/jbmc_parse_options.cpp

@@ -878,6 +878,7 @@ void jbmc_parse_optionst::help()
 
   std::cout << "   * *\n";
 
+  // clang-format off
   std::cout <<
     "* *              Daniel Kroening, Edmund Clarke             * *\n"
     "* * Carnegie Mellon University, Computer Science Department * *\n"
@@ -889,7 +890,7 @@ void jbmc_parse_optionst::help()
     " jbmc class                   name of class to be checked\n"
     "\n"
     "Analysis options:\n"
-    " --show-properties            show the properties, but don't run analysis\n" // NOLINT(*)
+    HELP_SHOW_PROPERTIES
     " --symex-coverage-report f    generate a Cobertura XML coverage report in f\n" // NOLINT(*)
     " --property id                only check one specific property\n"
     " --stop-on-fail               stop analysis once a failed property is detected\n" // NOLINT(*)
@@ -962,4 +963,5 @@ void jbmc_parse_optionst::help()
     " --verbosity #                verbosity level\n"
     HELP_TIMESTAMP
     "\n";
+  // clang-format on
 }

src/jbmc/jbmc_parse_options.h

@@ -22,6 +22,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <goto-programs/goto_trace.h>
 #include <goto-programs/lazy_goto_model.h>
+#include <goto-programs/show_properties.h>
 
 #include <java_bytecode/java_bytecode_language.h>
 
@@ -55,7 +56,7 @@ class optionst;
   OPT_SHOW_GOTO_FUNCTIONS \
   "(show-loops)" \
   "(show-symbol-table)(show-parse-tree)(show-vcc)" \
-  "(show-properties)" \
+  OPT_SHOW_PROPERTIES \
   "(drop-unused-functions)" \
   "(property):(stop-on-fail)(trace)" \
   "(verbosity):" \