Synchronise help output with actual support for --fp-reachability-slice

Neither CBMC nor JBMC actually interpret this option, despite it being
advertised in help output (and man pages). Conversely, goto-instrument
has support for `--reachability-slice-fb`, but it wasn't available on
the command line.

Author: tautschnig

doc/man/cbmc.1

@@ -258,12 +258,6 @@ set malloc failure mode to return null
 \fB\-\-string\-abstraction\fR
 track C string lengths and zero\-termination
 .TP
-\fB\-\-fp\-reachability\-slice\fR f
-remove instructions that cannot appear on a trace
-that visits all given functions. The list of
-functions has to be given as a comma separated
-list f.
-.TP
 \fB\-\-reachability\-slice\fR
 remove instructions that cannot appear on a trace
 from entry point to a property

doc/man/goto-instrument.1

@@ -972,6 +972,10 @@ list \fIf\fR.
 remove instructions that cannot appear on a trace
 from entry point to a property
 .TP
+\fB\-\-reachability\-slice\-fb\fR
+remove instructions that cannot appear on a trace
+from entry point through a property
+.TP
 \fB\-\-full\-slice\fR
 slice away instructions that don't affect assertions
 .TP

doc/man/jbmc.1

@@ -138,12 +138,6 @@ ignore user assumptions
 \fB\-\-mm\fR MM
 memory consistency model for concurrent programs
 .TP
-\fB\-\-fp\-reachability\-slice\fR f
-remove instructions that cannot appear on a trace
-that visits all given functions. The list of
-functions has to be given as a comma separated
-list f.
-.TP
 \fB\-\-reachability\-slice\fR
 remove instructions that cannot appear on a trace
 from entry point to a property

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -967,7 +967,6 @@ void jbmc_parse_optionst::help()
     " --no-assumptions             ignore user assumptions\n"
     " --mm MM                      memory consistency model for concurrent programs\n" // NOLINT(*)
     HELP_REACHABILITY_SLICER
-    HELP_REACHABILITY_SLICER_FB
     " --full-slice                 run full slicer (experimental)\n" // NOLINT(*)
     "\n"
     "Java Bytecode frontend options:\n"

src/cbmc/cbmc_parse_options.cpp

@@ -902,7 +902,6 @@ void cbmc_parse_optionst::help()
     " --mm MM                      memory consistency model for concurrent programs (default: sc)\n" // NOLINT(*)
     HELP_CONFIG_LIBRARY
     HELP_REACHABILITY_SLICER
-    HELP_REACHABILITY_SLICER_FB
     " --full-slice                 run full slicer (experimental)\n" // NOLINT(*)
     " --drop-unused-functions      drop functions trivially unreachable from main function\n" // NOLINT(*)
     " --havoc-undefined-functions\n"

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -95,7 +95,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "nondet_volatile.h"
 #include "points_to.h"
 #include "race_check.h"
-#include "reachability_slicer.h"
 #include "remove_function.h"
 #include "rw_set.h"
 #include "show_locations.h"
@@ -1971,6 +1970,7 @@ void goto_instrument_parse_optionst::help()
     "\n"
     "Slicing:\n"
     HELP_REACHABILITY_SLICER
+    HELP_FP_REACHABILITY_SLICER
     " --full-slice                 slice away instructions that don't affect assertions\n" // NOLINT(*)
     " --property id                slice with respect to specific property only\n" // NOLINT(*)
     " --slice-global-inits         slice away initializations of unused global variables\n" // NOLINT(*)

src/goto-instrument/goto_instrument_parse_options.h

@@ -36,6 +36,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "generate_function_bodies.h"
 #include "insert_final_assert_false.h"
 #include "nondet_volatile.h"
+#include "reachability_slicer.h"
 #include "replace_calls.h"
 #include "uninitialized.h"
 #include "unwindset.h"
@@ -77,8 +78,9 @@ Author: Daniel Kroening, kroening@kroening.com
   "(custom-bitvector-analysis)" \
   "(show-struct-alignment)(interval-analysis)(show-intervals)" \
   "(show-uninitialized)(show-locations)" \
-  "(full-slice)(reachability-slice)(slice-global-inits)" \
-  "(fp-reachability-slice):" \
+  "(full-slice)(slice-global-inits)" \
+  OPT_REACHABILITY_SLICER \
+  OPT_FP_REACHABILITY_SLICER \
   "(inline)(partial-inline)(function-inline):(log):(no-caching)" \
   "(value-set-fi-fp-removal)" \
   OPT_REMOVE_CONST_FUNCTION_POINTERS \

src/goto-instrument/reachability_slicer.h

@@ -42,18 +42,18 @@ void reachability_slicer(
   message_handlert &);
 
 // clang-format off
-#define OPT_REACHABILITY_SLICER                                                \
-  "(fp-reachability-slice):(reachability-slice)(reachability-slice-fb)" // NOLINT(*)
-
-#define HELP_REACHABILITY_SLICER                                                      \
-  " --fp-reachability-slice f    remove instructions that cannot appear on a trace\n" \
-  "                              that visits all given functions. The list of\n"      \
-  "                              functions has to be given as a comma separated\n"    \
-  "                              list f.\n"                                           \
-  " --reachability-slice         remove instructions that cannot appear on a trace\n" \
-  "                              from entry point to a property\n" // NOLINT(*)
-#define HELP_REACHABILITY_SLICER_FB                                                   \
-  " --reachability-slice-fb      remove instructions that cannot appear on a trace\n" \
-  "                              from entry point through a property\n" // NOLINT(*)
+#define OPT_FP_REACHABILITY_SLICER "(fp-reachability-slice):"
+#define OPT_REACHABILITY_SLICER "(reachability-slice)(reachability-slice-fb)"
+
+#define HELP_FP_REACHABILITY_SLICER \
+  " --fp-reachability-slice f    remove instructions that cannot appear on\n" \
+  "                              trace that visits all given functions.\n" \
+  "                              The list of functions has to be given as a\n" \
+  "                              comma separated list f.\n"
+#define HELP_REACHABILITY_SLICER \
+  " --reachability-slice         remove instructions that cannot appear on\n" \
+  "                              a trace from entry point to a property\n" \
+  " --reachability-slice-fb      remove instructions that cannot appear on\n" \
+  "                              a trace from entry point through a property\n"
 // clang-format on
 #endif // CPROVER_GOTO_INSTRUMENT_REACHABILITY_SLICER_H