Skip to content

Commit 9623aa5

Browse files
author
Daniel Kroening
committed
remove slice_by_trace feature
This feature has no known users, and the code has no maintainer.
1 parent 18cb59a commit 9623aa5

File tree

6 files changed

+4
-687
lines changed

6 files changed

+4
-687
lines changed

src/cbmc/cbmc_parse_options.cpp

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -234,7 +234,10 @@ void cbmc_parse_optionst::get_command_line_options(optionst &options)
234234
options.set_option("debug-level", cmdline.get_value("debug-level"));
235235

236236
if(cmdline.isset("slice-by-trace"))
237-
options.set_option("slice-by-trace", cmdline.get_value("slice-by-trace"));
237+
{
238+
error() << "--slice-by-trace has been removed" << eom;
239+
exit(CPROVER_EXIT_USAGE_ERROR);
240+
}
238241

239242
if(cmdline.isset("unwindset"))
240243
options.set_option("unwindset", cmdline.get_value("unwindset"));

src/goto-checker/bmc_util.cpp

Lines changed: 0 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,6 @@ Author: Daniel Kroening, Peter Schrammel
2121
#include <goto-symex/build_goto_trace.h>
2222
#include <goto-symex/memory_model_pso.h>
2323
#include <goto-symex/slice.h>
24-
#include <goto-symex/slice_by_trace.h>
2524
#include <goto-symex/symex_target_equation.h>
2625

2726
#include <linking/static_lifetime_init.h>
@@ -187,13 +186,7 @@ void slice(
187186
ui_message_handlert &ui_message_handler)
188187
{
189188
messaget msg(ui_message_handler);
190-
if(options.get_option("slice-by-trace") != "")
191-
{
192-
symex_slice_by_tracet symex_slice_by_trace(ns);
193189

194-
symex_slice_by_trace.slice_by_trace(
195-
options.get_option("slice-by-trace"), symex_target_equation);
196-
}
197190
// any properties to check at all?
198191
if(symex_target_equation.has_threads())
199192
{

src/goto-diff/goto_diff_parse_options.cpp

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -123,9 +123,6 @@ void goto_diff_parse_optionst::get_command_line_options(optionst &options)
123123
if(cmdline.isset("debug-level"))
124124
options.set_option("debug-level", cmdline.get_value("debug-level"));
125125

126-
if(cmdline.isset("slice-by-trace"))
127-
options.set_option("slice-by-trace", cmdline.get_value("slice-by-trace"));
128-
129126
if(cmdline.isset("unwindset"))
130127
options.set_option("unwindset", cmdline.get_value("unwindset"));
131128

src/goto-symex/Makefile

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -14,7 +14,6 @@ SRC = auto_objects.cpp \
1414
show_program.cpp \
1515
show_vcc.cpp \
1616
slice.cpp \
17-
slice_by_trace.cpp \
1817
symex_assign.cpp \
1918
symex_atomic_section.cpp \
2019
symex_builtin_functions.cpp \

0 commit comments

Comments
 (0)