Add --reachability-slice option warning

Author: NlightNFotis

doc/cprover-manual/unsound_options.md

@@ -7,6 +7,10 @@ have been reported to be unsound:
   In particular, `--full-slice` appears to lead to spurious counter examples,
   because values that get assigned by a function whose body gets sliced out are
   no longer present in the trace, but still result in flipped verification results.
+* `--reachability-slice` has been reported unsound at least once, in issue [cbmc#6394](https://github.com/diffblue/cbmc/issues/6394).
+  The state of this option these days is that this flag *should not* contain significant
+  soundness bugs, but it has a number of potential issues that pop up everyone now and then,
+  which renders it unsuitable for production use.
 
 `cbmc` and `goto-instrument` have also been modified to warn that options used
 are unsound as part of their output. An example of how that output looks is shown

src/cbmc/cbmc_parse_options.cpp

@@ -825,6 +825,11 @@ bool cbmc_parse_optionst::process_goto_program(
 
   if(options.get_bool_option("reachability-slice"))
   {
+    log.warning() << "**** WARNING: Unsound option `--reachability-slice'"
+                  << messaget::eom;
+    log.warning()
+      << "Please look at documentation file `unsound_options.md' for more info"
+      << messaget::eom;
     log.status() << "Performing a reachability slice" << messaget::eom;
     if(options.is_set("property"))
     {

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1711,6 +1711,12 @@ void goto_instrument_parse_optionst::instrument_goto_program()
   {
     do_indirect_call_and_rtti_removal();
 
+    log.warning() << "**** WARNING: Unsound option `--reachability-slice'"
+                  << messaget::eom;
+    log.warning()
+      << "Please look at documentation file `unsound_options.md' for more info"
+      << messaget::eom;
+
     log.status() << "Performing a reachability slice" << messaget::eom;
 
     // reachability_slicer requires that the model has unique location numbers: