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

Author: NlightNFotis

src/cbmc/cbmc_parse_options.cpp

@@ -840,6 +840,7 @@ 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,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" << messaget::eom;
     log.status() << "Performing a full slice" << messaget::eom;
+
     if(cmdline.isset("property"))
       property_slicer(goto_model, cmdline.get_values("property"));
     else
@@ -1806,6 +1808,7 @@ void goto_instrument_parse_optionst::instrument_goto_program()
     goto_model.goto_functions.update();
 
     log.status() << "Performing a reachability slice" << messaget::eom;
+
     if(cmdline.isset("property"))
     {
       reachability_slicer(