diff --git a/regression/goto-instrument/slice02/test.desc b/regression/goto-instrument/slice02/test.desc index 362da05d33c..2d61905c826 100644 --- a/regression/goto-instrument/slice02/test.desc +++ b/regression/goto-instrument/slice02/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.c --pointer-check --full-slice ^EXIT=0$ diff --git a/regression/goto-instrument/slice14/test.desc b/regression/goto-instrument/slice14/test.desc index ef912633761..a2b36885fc7 100644 --- a/regression/goto-instrument/slice14/test.desc +++ b/regression/goto-instrument/slice14/test.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE main.c --pointer-check --full-slice ^EXIT=10$ diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp index 4c080b10ceb..e33e700e0ca 100644 --- a/src/cbmc/cbmc_parse_options.cpp +++ b/src/cbmc/cbmc_parse_options.cpp @@ -900,13 +900,6 @@ bool cbmc_parse_optionst::process_goto_program( // Similar removal of RTTI inspection: remove_instanceof(symbol_table, goto_functions); - // full slice? - if(cmdline.isset("full-slice")) - { - status() << "Performing a full slice" << eom; - full_slicer(goto_functions, ns); - } - // do partial inlining status() << "Partial Inlining" << eom; goto_partial_inline(goto_functions, ns, ui_message_handler); @@ -920,6 +913,14 @@ bool cbmc_parse_optionst::process_goto_program( // add generic checks status() << "Generic Property Instrumentation" << eom; goto_check(ns, options, goto_functions); + + // full slice? + if(cmdline.isset("full-slice")) + { + status() << "Performing a full slice" << eom; + full_slicer(goto_functions, ns); + } + // checks don't know about adjusted float expressions adjust_float_expressions(goto_functions, ns); diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 209a5daeed1..594609ce8ce 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -1432,6 +1432,7 @@ void goto_instrument_parse_optionst::instrument_goto_program() // full slice? if(cmdline.isset("full-slice")) { + remove_returns(symbol_table, goto_functions); do_indirect_call_and_rtti_removal(); status() << "Performing a full slice" << eom;