consider array_set expressions in the full-slice (do not merge)

regression/cbmc-java/slice1/test.desc

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

regression/cbmc-java/slice1/testSlice.java

@@ -0,0 +1,31 @@
+class test
+{
+  public void f1()
+  {
+    int y=0;
+    y++;
+  }
+
+  public void f2()
+  {
+    i++;
+  }
+
+  public int f3()
+  {
+    return i;
+  }
+
+  private int i;
+}
+
+public class testSlice
+{
+  public static void main(String[] args)
+  {
+    test t = new test();
+    t.f1();
+    t.f2();
+    assert t.f3()==1;
+  }
+}

regression/goto-instrument/slice05/main.c

@@ -1,3 +1,5 @@
+#include <assert.h>
+
 int main()
 {
   int x = 1; /* considering changing this line */

regression/goto-instrument/slice07/test.desc

@@ -1,8 +1,6 @@
 KNOWNBUG
 main.c
 --full-slice
-^EXIT=6$
+^EXIT=0$
 ^SIGNAL=0$
-^\-\-full\-slice does not support C/Pthreads yet$
---
-^warning: ignoring
+^VERIFICATION SUCCESSFUL$

regression/goto-instrument/slice18/test.desc

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

regression/goto-instrument/slice24/main.c

@@ -0,0 +1,22 @@
+#include <assert.h>
+
+int x;
+
+void f1()
+{
+  int y=0;
+  y++;
+}
+
+void f2()
+{
+  x++;
+}
+
+int main()
+{
+  f1();
+  f2();
+  assert(x==1);
+  return 0;
+}

regression/goto-instrument/slice24/test.desc

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

src/cbmc/Makefile

@@ -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) \

src/cbmc/cbmc_parse_options.cpp

@@ -50,6 +50,7 @@ Author: Daniel Kroening, [email protected]
 #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);
 

src/goto-instrument/full_slicer.cpp

@@ -318,6 +318,8 @@ void full_slicert::operator()(
       const exprt &s=to_code_dead(e_it->first->code).symbol();
       decl_dead[to_symbol_expr(s).get_identifier()].push(e_it->second);
     }
+    else if(e_it->first->is_function_call())
+      add_to_queue(queue, e_it->second, e_it->first);
   }
 
   // compute program dependence graph (and post-dominators)

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -1410,16 +1410,6 @@ void goto_instrument_parse_optionst::instrument_goto_program()
     nondet_volatile(symbol_table, goto_functions);
   }
 
-  // reachability slice?
-  if(cmdline.isset("reachability-slice"))
-  {
-    status() << "Performing a reachability slice" << eom;
-    if(cmdline.isset("property"))
-      reachability_slicer(goto_functions, cmdline.get_values("property"));
-    else
-      reachability_slicer(goto_functions);
-  }
-
   // full slice?
   if(cmdline.isset("full-slice"))
   {
@@ -1433,6 +1423,19 @@ void goto_instrument_parse_optionst::instrument_goto_program()
       full_slicer(goto_functions, ns);
   }
 
+  // reachability slice?
+  if(cmdline.isset("reachability-slice") || cmdline.isset("full-slice"))
+  {
+    status() << "Performing a reachability slice" << eom;
+    if(cmdline.isset("property"))
+      reachability_slicer(goto_functions, cmdline.get_values("property"));
+    else
+      reachability_slicer(goto_functions);
+  }
+
+  // label the assertions
+  label_properties(goto_functions);
+
   // recalculate numbers, etc.
   goto_functions.update();
 }