Explain unsound options in documentation.

Author: NlightNFotis

doc/cprover-manual/unsound_options.md

@@ -0,0 +1,33 @@
+# Unsound CLI options for various tools
+
+Be advised that the following command line options to `cbmc` and `goto-instrument`
+have been reported to be unsound:
+
+* `--full-slice` has been reported to be unsound in issue [cbmc#260](https://github.com/diffblue/cbmc/issues/260)
+  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.
+
+`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
+below:
+
+```sh
+$ cbmc --full-slice ~/Devel/cbmc_bugs/6394/before-slice.out
+CBMC version 5.45.0 (cbmc-5.43.0-77-g99c5a92de1-dirty) 64-bit arm64 macos
+Reading GOTO program from file
+Reading: ~/Devel/cbmc_bugs/6394/before-slice.out
+Generating GOTO Program
+Adding CPROVER library (x86_64)
+Removal of function pointers and virtual functions
+Generic Property Instrumentation
+WARNING: Unsound option --full-slice
+Performing a full slice
+Running with 8 object bits, 56 offset bits (default)
+Starting Bounded Model Checking
+[...]
+```
+
+Be advised some of these options may be activated by auxiliary options, for instance,
+`--aggressive-slice` seems to lead to a path that performs the transformations that
+`--reachability-slice` does in `goto-instrument`.