Distinguish intentionally unsound from experimental options

tautschnig · tautschnig · commit 2f723d59246c · 2023-02-23T20:30:35.000Z
Unlike some other options (which are yet to be documented),
`--full-slice` is not unsound by design.
diff --git a/doc/cprover-manual/unsound_options.md b/doc/cprover-manual/unsound_options.md
@@ -15,13 +15,14 @@ that we want to avoid:
 * **Wrong proof to an assertion**, which means that it might indicate an assertion passing
   when it's not.
 
-We expect core CBMC to display none of the behaviour we described above (and if it does,
+We expect that, by default, CBMC displays none of the behaviour we described above (and if it does,
 it's an extremely serious bug that we aim to fix on an ASAP basis), but be aware that
 certain tools, like `goto-instrument`, may contain components that are experimental in
 nature and thus do transformations that eventually lead to behaviour such as the ones
-described above.
+described above. Furthermore, there are some options that lead to unsound
+analysis results *by design*.
 
-## Unsound Options
+## Experimental Options
 
 Be advised that the following command line options to `cbmc` and `goto-instrument`
 have been reported to be unsound:
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
@@ -840,7 +840,9 @@ bool cbmc_parse_optionst::process_goto_program(
   // full slice?
   if(options.get_bool_option("full-slice"))
   {
-    log.warning() << "**** WARNING: Unsound option --full-slice"
+    log.warning() << "**** WARNING: Experimental option --full-slice, "
+                  << "analysis results may be unsound. See "
+                  << "https://github.com/diffblue/cbmc/issues/260"
                   << messaget::eom;
     log.status() << "Performing a full slice" << messaget::eom;
     if(options.is_set("property"))
diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp
@@ -1743,7 +1743,9 @@ void goto_instrument_parse_optionst::instrument_goto_program()
     do_indirect_call_and_rtti_removal();
     do_remove_returns();
 
-    log.warning() << "**** WARNING: Unsound option --full-slice"
+    log.warning() << "**** WARNING: Experimental option --full-slice, "
+                  << "analysis results may be unsound. See "
+                  << "https://github.com/diffblue/cbmc/issues/260"
                   << messaget::eom;
     log.status() << "Performing a full slice" << messaget::eom;
     if(cmdline.isset("property"))
