Constify slicing_criteriont::operator()

This enables us to use a const-ref in the reachability and full slicers.

Author: smowton

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;

src/goto-instrument/reachability_slicer.cpp

@@ -35,7 +35,7 @@ Author: Daniel Kroening, [email protected]
 std::vector<reachability_slicert::cfgt::node_indext>
 reachability_slicert::get_sources(
   const is_threadedt &is_threaded,
-  slicing_criteriont &criterion)
+  const slicing_criteriont &criterion)
 {
   std::vector<cfgt::node_indext> sources;
   for(const auto &e_it : cfg.entry_map)
@@ -164,7 +164,7 @@ void reachability_slicert::backward_inwards_walk_from(
 /// \param criterion the criterion we are trying to hit
 void reachability_slicert::fixedpoint_to_assertions(
   const is_threadedt &is_threaded,
-  slicing_criteriont &criterion)
+  const slicing_criteriont &criterion)
 {
   std::vector<cfgt::node_indext> sources = get_sources(is_threaded, criterion);
 
@@ -302,7 +302,7 @@ void reachability_slicert::forward_inwards_walk_from(
 /// \param criterion the criterion we are trying to hit
 void reachability_slicert::fixedpoint_from_assertions(
   const is_threadedt &is_threaded,
-  slicing_criteriont &criterion)
+  const slicing_criteriont &criterion)
 {
   std::vector<cfgt::node_indext> sources = get_sources(is_threaded, criterion);
 

src/goto-instrument/reachability_slicer_class.h

@@ -24,7 +24,7 @@ class reachability_slicert
 public:
   void operator()(
     goto_functionst &goto_functions,
-    slicing_criteriont &criterion,
+    const slicing_criteriont &criterion,
     bool include_forward_reachability)
   {
     cfg(goto_functions);
@@ -76,11 +76,11 @@ class reachability_slicert
 
   void fixedpoint_to_assertions(
     const is_threadedt &is_threaded,
-    slicing_criteriont &criterion);
+    const slicing_criteriont &criterion);
 
   void fixedpoint_from_assertions(
     const is_threadedt &is_threaded,
-    slicing_criteriont &criterion);
+    const slicing_criteriont &criterion);
 
   void slice(goto_functionst &goto_functions);
 
@@ -100,8 +100,9 @@ class reachability_slicert
     std::vector<cfgt::node_indext> &callsite_successor_stack,
     std::vector<cfgt::node_indext> &callee_head_stack);
 
-  std::vector<cfgt::node_indext>
-  get_sources(const is_threadedt &is_threaded, slicing_criteriont &criterion);
+  std::vector<cfgt::node_indext> get_sources(
+    const is_threadedt &is_threaded,
+    const slicing_criteriont &criterion);
 };
 
 #endif // CPROVER_GOTO_INSTRUMENT_REACHABILITY_SLICER_CLASS_H