Mark --full-slice as unsound in cbmc and goto-instrument output.

Author: NlightNFotis

src/cbmc/cbmc_parse_options.cpp

@@ -840,6 +840,8 @@ bool cbmc_parse_optionst::process_goto_program(
   // full slice?
   if(options.get_bool_option("full-slice"))
   {
+    log.warning() << "**** WARNING: Unsound option --full-slice"
+                  << messaget::eom;
     log.status() << "Performing a full slice" << messaget::eom;
     if(options.is_set("property"))
       property_slicer(goto_model, options.get_list_option("property"));

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1743,6 +1743,8 @@ void goto_instrument_parse_optionst::instrument_goto_program()
     do_indirect_call_and_rtti_removal();
     do_remove_returns();
 
+    log.warning() << "**** WARNING: Unsound option --full-slice"
+                  << messaget::eom;
     log.status() << "Performing a full slice" << messaget::eom;
     if(cmdline.isset("property"))
       property_slicer(goto_model, cmdline.get_values("property"));