combined full-slice with reachability-slice

Author: lucasccordeiro

regression/cbmc-java/slice1/test.desc

@@ -0,0 +1,6 @@
+KNOWNBUG
+testSlice.class
+--full-slice
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$

regression/goto-instrument/slice24/testSlice.class renamed to regression/cbmc-java/slice1/testSlice.class

@@ -12,20 +12,16 @@ name=${name%.c}
 
 args=${@:1:$#-1}
 
-if [ -f $name.c ] ; then
-  $goto_cc -o $name.gb $name.c
+$goto_cc -o $name.gb $name.c
 # $goto_instrument --show-goto-functions $name.gb
-  $goto_instrument $args $name.gb ${name}-mod.gb
-  if [ ! -e ${name}-mod.gb ] ; then
-    cp $name.gb ${name}-mod.gb
-  elif echo "$args" | grep -q -- "--dump-c" ; then
-    mv ${name}-mod.gb ${name}-mod.c
-    $goto_cc ${name}-mod.c -o ${name}-mod.gb
-    rm ${name}-mod.c
-  fi
+$goto_instrument $args $name.gb ${name}-mod.gb
+if [ ! -e ${name}-mod.gb ] ; then
+  cp $name.gb ${name}-mod.gb
+elif echo "$args" | grep -q -- "--dump-c" ; then
+  mv ${name}-mod.gb ${name}-mod.c
+  $goto_cc ${name}-mod.c -o ${name}-mod.gb
+  rm ${name}-mod.c
+fi
 $goto_instrument --show-goto-functions ${name}-mod.gb
 $cbmc ${name}-mod.gb
-else
-  $cbmc $name
-fi
 

regression/goto-instrument/slice24/testSlice.java renamed to regression/cbmc-java/slice1/testSlice.java

@@ -1,6 +1,6 @@
-KNOWNBUG
-testSlice.class
+CORE
+main.c
 --full-slice
-^EXIT=10$
+^EXIT=0$
 ^SIGNAL=0$
-^VERIFICATION FAILED$
+^VERIFICATION SUCCESSFUL$

regression/goto-instrument/chain.sh

@@ -32,6 +32,7 @@ OBJ += ../ansi-c/ansi-c$(LIBEXT) \
       ../pointer-analysis/rewrite_index$(OBJEXT) \
       ../pointer-analysis/goto_program_dereference$(OBJEXT) \
       ../goto-instrument/full_slicer$(OBJEXT) \
+      ../goto-instrument/reachability_slicer$(OBJEXT) \
       ../goto-instrument/nondet_static$(OBJEXT) \
       ../goto-instrument/cover$(OBJEXT) \
       ../analyses/analyses$(LIBEXT) \

regression/goto-instrument/slice25/main.c renamed to regression/goto-instrument/slice24/main.c

@@ -50,6 +50,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-symex/adjust_float_expressions.h>
 
 #include <goto-instrument/full_slicer.h>
+#include <goto-instrument/reachability_slicer.h>
 #include <goto-instrument/nondet_static.h>
 #include <goto-instrument/cover.h>
 
@@ -821,6 +822,19 @@ bool cbmc_parse_optionst::process_goto_program(
     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);
+
+      status() << "Performing a reachability slice" << eom;
+       if(cmdline.isset("property"))
+         reachability_slicer(goto_functions, cmdline.get_values("property"));
+       else
+         reachability_slicer(goto_functions);
+    }
+
     // checks don't know about adjusted float expressions
     adjust_float_expressions(goto_functions, ns);
 

regression/goto-instrument/slice24/test.desc

@@ -17,7 +17,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-programs/remove_skip.h>
 
 #include "full_slicer_class.h"
-#include <iostream>
 
 void full_slicert::add_dependencies(
   const cfgt::nodet &node,