Invoked full_slicer after generic property intrumentation

Invoked the full_slicer method just after generic property instrumentation
so that CBMC can properly slice the program w.r.t. a given assertion in the program.
Additionally, replaced returns from goto functions in goto_instrument_parse_options,
as done similarly in cbmc_parse_options

Author: lucasccordeiro

regression/goto-instrument/slice02/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --pointer-check --full-slice
 ^EXIT=0$

regression/goto-instrument/slice14/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --pointer-check --full-slice
 ^EXIT=10$

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);
 

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;