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

Author: NlightNFotis

src/cbmc/cbmc_parse_options.cpp

@@ -952,6 +952,8 @@ bool cbmc_parse_optionst::process_goto_program(
 
   if(options.get_bool_option("reachability-slice"))
   {
+    log.warning() << "WARNING: Unsound option --reachability-slice"
+                  << messaget::eom;
     log.status() << "Performing a reachability slice" << messaget::eom;
     if(options.is_set("property"))
       reachability_slicer(goto_model, options.get_list_option("property"));
@@ -962,6 +964,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

@@ -1596,6 +1596,8 @@ void goto_instrument_parse_optionst::instrument_goto_program()
   {
     do_indirect_call_and_rtti_removal();
 
+    log.warning() << "WARNING: Unsound option --reachability-slice"
+                  << messaget::eom;
     log.status() << "Performing a reachability slice" << messaget::eom;
 
     // reachability_slicer requires that the model has unique location numbers:
@@ -1623,7 +1625,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
@@ -1685,7 +1689,10 @@ void goto_instrument_parse_optionst::instrument_goto_program()
 
     goto_model.goto_functions.update();
 
+    log.warning() << "WARNING: Unsound option --reachability-slice"
+                  << messaget::eom;
     log.status() << "Performing a reachability slice" << messaget::eom;
+
     if(cmdline.isset("property"))
       reachability_slicer(goto_model, cmdline.get_values("property"));
     else