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

Author: NlightNFotis

src/cbmc/cbmc_parse_options.cpp

@@ -955,6 +955,7 @@ 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"));
@@ -965,6 +966,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

@@ -1600,6 +1600,7 @@ 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:
@@ -1627,7 +1628,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
@@ -1689,7 +1692,9 @@ 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