Merge pull request #3971 from diffblue/remove_slice_by_trace

remove slice_by_trace feature

Author: tautschnig

jbmc/src/jbmc/jbmc_parse_options.cpp

@@ -172,9 +172,6 @@ void jbmc_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("debug-level"))
     options.set_option("debug-level", cmdline.get_value("debug-level"));
 
-  if(cmdline.isset("slice-by-trace"))
-    options.set_option("slice-by-trace", cmdline.get_value("slice-by-trace"));
-
   if(cmdline.isset("unwindset"))
     options.set_option("unwindset", cmdline.get_value("unwindset"));
 

jbmc/src/jbmc/jbmc_parse_options.h

@@ -40,7 +40,7 @@ class optionst;
 // clang-format off
 #define JBMC_OPTIONS \
   OPT_BMC \
-  "(preprocess)(slice-by-trace):" \
+  "(preprocess)" \
   OPT_FUNCTIONS \
   "(no-simplify)(full-slice)" \
   OPT_REACHABILITY_SLICER \

jbmc/src/jdiff/jdiff_parse_options.cpp

@@ -112,9 +112,6 @@ void jdiff_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("debug-level"))
     options.set_option("debug-level", cmdline.get_value("debug-level"));
 
-  if(cmdline.isset("slice-by-trace"))
-    options.set_option("slice-by-trace", cmdline.get_value("slice-by-trace"));
-
   if(cmdline.isset("unwindset"))
     options.set_option("unwindset", cmdline.get_value("unwindset"));
 

src/cbmc/cbmc_parse_options.cpp

@@ -238,7 +238,10 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
     options.set_option("debug-level", cmdline.get_value("debug-level"));
 
   if(cmdline.isset("slice-by-trace"))
-    options.set_option("slice-by-trace", cmdline.get_value("slice-by-trace"));
+  {
+    error() << "--slice-by-trace has been removed" << eom;
+    exit(CPROVER_EXIT_USAGE_ERROR);
+  }
 
   if(cmdline.isset("unwindset"))
     options.set_option("unwindset", cmdline.get_value("unwindset"));

src/goto-checker/bmc_util.cpp

@@ -21,7 +21,6 @@ Author: Daniel Kroening, Peter Schrammel
 #include <goto-symex/build_goto_trace.h>
 #include <goto-symex/memory_model_pso.h>
 #include <goto-symex/slice.h>
-#include <goto-symex/slice_by_trace.h>
 #include <goto-symex/symex_target_equation.h>
 
 #include <linking/static_lifetime_init.h>
@@ -187,13 +186,7 @@ void slice(
   ui_message_handlert &ui_message_handler)
 {
   messaget msg(ui_message_handler);
-  if(options.get_option("slice-by-trace") != "")
-  {
-    symex_slice_by_tracet symex_slice_by_trace(ns);
 
-    symex_slice_by_trace.slice_by_trace(
-      options.get_option("slice-by-trace"), symex_target_equation);
-  }
   // any properties to check at all?
   if(symex_target_equation.has_threads())
   {

src/goto-diff/goto_diff_parse_options.cpp

@@ -127,9 +127,6 @@ void goto_diff_parse_optionst::get_command_line_options(optionst &options)
   if(cmdline.isset("debug-level"))
     options.set_option("debug-level", cmdline.get_value("debug-level"));
 
-  if(cmdline.isset("slice-by-trace"))
-    options.set_option("slice-by-trace", cmdline.get_value("slice-by-trace"));
-
   if(cmdline.isset("unwindset"))
     options.set_option("unwindset", cmdline.get_value("unwindset"));
 

src/goto-symex/Makefile

@@ -14,7 +14,6 @@ SRC = auto_objects.cpp \
       show_program.cpp \
       show_vcc.cpp \
       slice.cpp \
-      slice_by_trace.cpp \
       symex_assign.cpp \
       symex_atomic_section.cpp \
       symex_builtin_functions.cpp \