Skip to content

Commit 0376eab

Browse files
committed
rename command line options for aggressive slicer
1 parent c469d3d commit 0376eab

File tree

5 files changed

+23
-19
lines changed

5 files changed

+23
-19
lines changed

regression/goto-instrument/aggressive_slicer4/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main.c
3-
--aggressive-slice --preserve-function B
3+
--aggressive-slice --aggressive-slice-preserve-function B
44
^EXIT=10$
55
^SIGNAL=0$
66
^VERIFICATION FAILED$

regression/goto-instrument/aggressive_slicer5/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main.c
3-
--aggressive-slice --property D.assertion.1 --preserve-all-direct-paths
3+
--aggressive-slice --property D.assertion.1 --aggressive-slice-preserve-all-direct-paths
44
^EXIT=10$
55
^SIGNAL=0$
66
^VERIFICATION FAILED$

regression/goto-instrument/aggressive_slicer6/test.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
CORE
22
main.c
3-
--aggressive-slice --call-depth 1
3+
--aggressive-slice --aggressive-slice-call-depth 1
44
^EXIT=10$
55
^SIGNAL=0$
66
^VERIFICATION FAILED$

src/goto-instrument/goto_instrument_parse_options.cpp

Lines changed: 16 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -1474,24 +1474,24 @@ void goto_instrument_parse_optionst::instrument_goto_program()
14741474
status() << "Performing an aggressive slice" << eom;
14751475
aggressive_slicert aggressive_slicer(goto_model, get_message_handler());
14761476

1477-
if(cmdline.isset("call-depth"))
1477+
if(cmdline.isset("aggressive-slice-call-depth"))
14781478
aggressive_slicer.call_depth =
1479-
safe_string2unsigned(cmdline.get_value("call-depth"));
1479+
safe_string2unsigned(cmdline.get_value("aggressive-slice-call-depth"));
14801480

1481-
if(cmdline.isset("preserve-function"))
1481+
if(cmdline.isset("aggressive-slice-preserve-function"))
14821482
aggressive_slicer.preserve_functions(
1483-
cmdline.get_values("preserve-function"));
1483+
cmdline.get_values("aggressive-slice-preserve-function"));
14841484

14851485
if(cmdline.isset("property"))
14861486
aggressive_slicer.user_specified_properties =
14871487
cmdline.get_values("property");
14881488

1489-
if(cmdline.isset("preserve-functions-containing"))
1489+
if(cmdline.isset("aggressive-slice-preserve-functions-containing"))
14901490
aggressive_slicer.name_snippets =
1491-
cmdline.get_values("preserve-functions-containing");
1491+
cmdline.get_values("aggressive-slice-preserve-functions-containing");
14921492

14931493
aggressive_slicer.preserve_all_direct_paths =
1494-
cmdline.isset("preserve-all-direct-paths");
1494+
cmdline.isset("aggressive-slice-preserve-all-direct-paths");
14951495

14961496
aggressive_slicer.doit();
14971497

@@ -1607,14 +1607,18 @@ void goto_instrument_parse_optionst::help()
16071607
" --full-slice slice away instructions that don't affect assertions\n" // NOLINT(*)
16081608
" --property id slice with respect to specific property only\n" // NOLINT(*)
16091609
" --slice-global-inits slice away initializations of unused global variables\n" // NOLINT(*)
1610-
" --aggressive-slice remove bodies of any functions not on the shortest path between\n" // NOLINT(*)
1610+
" --aggressive-slice-aggressive-slice \n"
1611+
" remove bodies of any functions not on the shortest path between\n" // NOLINT(*)
16111612
" the start function and the function containing the property(s)\n" // NOLINT(*)
1612-
" --call-depth <n> used with aggressive-slice, preserves all functions within <n> function calls\n" // NOLINT(*)
1613+
" --aggressive-slice-call-depth <n> \n"
1614+
" used with aggressive-slice, preserves all functions within <n> function calls\n" // NOLINT(*)
16131615
" of the functions on the shortest path\n"
1614-
" --preserve-function <f> force the aggressive slicer to preserve function <f>\n" // NOLINT(*)
1615-
" --preserve-function containing <f>\n"
1616+
" --aggressive-slice-preserve-function <f> \n"
1617+
" force the aggressive slicer to preserve function <f>\n" // NOLINT(*)
1618+
" --aggressive-slice-preserve-function containing <f>\n"
16161619
" force the aggressive slicer to preserve all functions with names containing <f>\n" // NOLINT(*)
1617-
"--preserve-all-direct-paths force aggressive slicer to preserve all direct paths\n" // NOLINT(*)
1620+
"--aggressive-slice-preserve-all-direct-paths \n"
1621+
" force aggressive slicer to preserve all direct paths\n" // NOLINT(*)
16181622
"\n"
16191623
"Further transformations:\n"
16201624
" --constant-propagator propagate constants and simplify expressions\n" // NOLINT(*)

src/goto-instrument/goto_instrument_parse_options.h

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -91,10 +91,10 @@ Author: Daniel Kroening, [email protected]
9191
"(undefined-function-is-assume-false)" \
9292
"(remove-function-body):"\
9393
"(aggressive-slice)" \
94-
"(call-depth):" \
95-
"(preserve-function):" \
96-
"(preserve-functions-containing):" \
97-
"(preserve-all-direct-paths)" \
94+
"(aggressive-slice-call-depth):" \
95+
"(aggressive-slice-preserve-function):" \
96+
"(aggressive-slice-preserve-functions-containing):" \
97+
"(aggressive-slice-preserve-all-direct-paths)" \
9898
OPT_FLUSH \
9999
"(splice-call):" \
100100
OPT_REMOVE_CALLS_NO_BODY \

0 commit comments

Comments
 (0)