Merge pull request #3218 from smowton/smowton/fix/reachability-slicer-take-3

Reachability slicer: split cfg walks into two phases

Author: smowton

regression/cbmc/reachability-slice-interproc2/main.c

@@ -0,0 +1,23 @@
+void b();
+
+void c()
+{
+  __CPROVER_assert(0, "");
+  b();
+}
+
+void b()
+{
+  a();
+  c();
+}
+
+void a()
+{
+  c();
+}
+
+int main()
+{
+  a();
+}

regression/cbmc/reachability-slice-interproc2/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--reachability-slice --show-goto-functions
+^EXIT=0$
+^SIGNAL=0$
+main\(\)
+--
+^warning: ignoring

regression/cbmc/reachability-slice-interproc3/main.c

@@ -0,0 +1,19 @@
+void intermediate();
+void root();
+
+int main()
+{
+  intermediate();
+  return 1;
+}
+
+void intermediate()
+{
+  root();
+}
+
+void root()
+{
+  __CPROVER_assert(0, "");
+  intermediate();
+}

regression/cbmc/reachability-slice-interproc3/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--reachability-slice-fb --show-goto-functions
+^EXIT=0$
+^SIGNAL=0$
+main#return_value = 1;
+--
+^warning: ignoring

src/goto-instrument/full_slicer.cpp

@@ -284,7 +284,7 @@ static bool implicit(goto_programt::const_targett target)
 void full_slicert::operator()(
   goto_functionst &goto_functions,
   const namespacet &ns,
-  slicing_criteriont &criterion)
+  const slicing_criteriont &criterion)
 {
   // build the CFG data structure
   cfg(goto_functions);
@@ -367,7 +367,7 @@ void full_slicert::operator()(
 void full_slicer(
   goto_functionst &goto_functions,
   const namespacet &ns,
-  slicing_criteriont &criterion)
+  const slicing_criteriont &criterion)
 {
   full_slicert()(goto_functions, ns, criterion);
 }

src/goto-instrument/full_slicer.h

@@ -33,12 +33,12 @@ class slicing_criteriont
 {
 public:
   virtual ~slicing_criteriont();
-  virtual bool operator()(goto_programt::const_targett)=0;
+  virtual bool operator()(goto_programt::const_targett) const = 0;
 };
 
 void full_slicer(
   goto_functionst &goto_functions,
   const namespacet &ns,
-  slicing_criteriont &criterion);
+  const slicing_criteriont &criterion);
 
 #endif // CPROVER_GOTO_INSTRUMENT_FULL_SLICER_H

src/goto-instrument/full_slicer_class.h

@@ -41,7 +41,7 @@ class full_slicert
   void operator()(
     goto_functionst &goto_functions,
     const namespacet &ns,
-    slicing_criteriont &criterion);
+    const slicing_criteriont &criterion);
 
 protected:
   struct cfg_nodet
@@ -107,7 +107,7 @@ class full_slicert
 class assert_criteriont:public slicing_criteriont
 {
 public:
-  virtual bool operator()(goto_programt::const_targett target)
+  virtual bool operator()(goto_programt::const_targett target) const
   {
     return target->is_assert();
   }
@@ -121,7 +121,7 @@ class in_function_criteriont : public slicing_criteriont
   {
   }
 
-  virtual bool operator()(goto_programt::const_targett target)
+  virtual bool operator()(goto_programt::const_targett target) const
   {
     return target->function == target_function;
   }
@@ -139,7 +139,7 @@ class properties_criteriont:public slicing_criteriont
   {
   }
 
-  virtual bool operator()(goto_programt::const_targett target)
+  virtual bool operator()(goto_programt::const_targett target) const
   {
     if(!target->is_assert())
       return false;