Add context_abstract_object::to_predicate

Relax to_predicate visibility from private to protected to enable this.

Author: jezhiggins

src/analyses/variable-sensitivity/abstract_object.h

@@ -363,6 +363,11 @@ class abstract_objectt : public std::enable_shared_from_this<abstract_objectt>
     return shared_from_this() == other;
   }
 
+  /// to_predicate implementation - derived classes will override
+  /// \param name - the variable name to substitute into the expression
+  /// \return Returns an exprt representing the object as an invariant.
+  virtual exprt to_predicate_internal(const exprt &name) const;
+
 private:
   /// To enforce copy-on-write these are private and have read-only accessors
   typet t;
@@ -378,11 +383,6 @@ class abstract_objectt : public std::enable_shared_from_this<abstract_objectt>
   {
   }
 
-  /// to_predicate implementation - derived classes will override
-  /// \param name - the variable name to substitute into the expression
-  /// \return Returns an exprt representing the object as an invariant.
-  virtual exprt to_predicate_internal(const exprt &name) const;
-
   /**
    * Helper function for abstract_objectt::abstract_object_merge to perform any
    * additional actions after the base abstract_object_merge has completed it's

src/analyses/variable-sensitivity/constant_abstract_value.h

@@ -81,9 +81,9 @@ class constant_abstract_valuet : public abstract_value_objectt
   abstract_object_pointert
   meet_with_value(const abstract_value_pointert &other) const override;
 
-private:
   exprt to_predicate_internal(const exprt &name) const override;
 
+private:
   exprt value;
 };
 

src/analyses/variable-sensitivity/context_abstract_object.cpp

@@ -160,6 +160,11 @@ abstract_object_pointert context_abstract_objectt::unwrap_context() const
   return child_abstract_object->unwrap_context();
 }
 
+exprt context_abstract_objectt::to_predicate_internal(const exprt &name) const
+{
+  return child_abstract_object->to_predicate(name);
+}
+
 void context_abstract_objectt::get_statistics(
   abstract_object_statisticst &statistics,
   abstract_object_visitedt &visited,

src/analyses/variable-sensitivity/context_abstract_object.h

@@ -117,6 +117,8 @@ class context_abstract_objectt : public abstract_objectt
     bool merging_write) const override;
 
   bool has_been_modified(const abstract_object_pointert &before) const override;
+
+  exprt to_predicate_internal(const exprt &name) const override;
 };
 
 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_CONTEXT_ABSTRACT_OBJECT_H

src/analyses/variable-sensitivity/interval_abstract_value.h

@@ -94,9 +94,9 @@ class interval_abstract_valuet : public abstract_value_objectt
   abstract_object_pointert
   meet_with_value(const abstract_value_pointert &other) const override;
 
-private:
   exprt to_predicate_internal(const exprt &name) const override;
 
+private:
   constant_interval_exprt interval;
 
   void set_top_internal() override;

src/analyses/variable-sensitivity/value_set_abstract_object.h

@@ -69,6 +69,8 @@ class value_set_abstract_objectt : public abstract_value_objectt,
   abstract_object_pointert
   meet_with_value(const abstract_value_pointert &other) const override;
 
+  exprt to_predicate_internal(const exprt &name) const override;
+
 private:
   /// Setter for updating the stored values
   /// \param other_values: the new (non-empty) set of values
@@ -84,8 +86,6 @@ class value_set_abstract_objectt : public abstract_value_objectt,
 
   void set_top_internal() override;
 
-  exprt to_predicate_internal(const exprt &name) const override;
-
   // data
   abstract_object_sett values;
 };