array_abstract_objectt::write_index returns abstract_object_pointert

Was returning a shared_ptr<const array_abstract_objectt>, but
write_index is only called from write, which returns an
abstract_object_pointert so returning the more specialised shared
pointer was redundant. This change will also allow the
write_index implementation to be simplified.

Author: jezhiggins

src/analyses/variable-sensitivity/array_abstract_object.cpp

@@ -68,7 +68,7 @@ abstract_object_pointert array_abstract_objectt::read_index(
   return env.abstract_object_factory(subtype, ns, !is_bottom(), is_bottom());
 }
 
-sharing_ptrt<array_abstract_objectt> array_abstract_objectt::write_index(
+abstract_object_pointert array_abstract_objectt::write_index(
   abstract_environmentt &environment,
   const namespacet &ns,
   const std::stack<exprt> stack,

src/analyses/variable-sensitivity/array_abstract_object.h

@@ -117,10 +117,10 @@ class array_abstract_objectt : public abstract_objectt
   /// \param value: the value we are trying to assign to that value in the array
   /// \param merging_write: ?
   ///
-  /// \return The array_abstract_objectt representing the result of writing
+  /// \return The abstract_object_pointert representing the result of writing
   ///          to a specific component. In this case this will always be top
   ///          as we are not tracking the value in the array.
-  virtual sharing_ptrt<array_abstract_objectt> write_index(
+  virtual abstract_object_pointert write_index(
     abstract_environmentt &environment,
     const namespacet &ns,
     const std::stack<exprt> stack,

src/analyses/variable-sensitivity/constant_array_abstract_object.cpp

@@ -189,7 +189,7 @@ abstract_object_pointert constant_array_abstract_objectt::read_index(
   }
 }
 
-sharing_ptrt<array_abstract_objectt>
+abstract_object_pointert
 constant_array_abstract_objectt::write_index(
   abstract_environmentt &environment,
   const namespacet &ns,

src/analyses/variable-sensitivity/constant_array_abstract_object.h

@@ -110,9 +110,9 @@ class constant_array_abstract_objectt : public array_abstract_objectt
   /// \param value: the value we are trying to assign to that value in the array
   /// \param merging_write: Should this and all future writes be merged with the
   ///                       current value
-  /// \return The array_abstract_objectt representing the result of writing
+  /// \return The abstract_object_pointert representing the result of writing
   ///         to a specific index.
-  sharing_ptrt<array_abstract_objectt> write_index(
+  abstract_object_pointert write_index(
     abstract_environmentt &environment,
     const namespacet &ns,
     const std::stack<exprt> stack,

src/analyses/variable-sensitivity/interval_array_abstract_object.cpp

@@ -47,7 +47,7 @@ static constant_interval_exprt eval_and_get_as_interval(
   return evaluated_index_interval->get_interval();
 }
 
-sharing_ptrt<array_abstract_objectt>
+abstract_object_pointert
 interval_array_abstract_objectt::write_index(
   abstract_environmentt &environment,
   const namespacet &ns,

src/analyses/variable-sensitivity/interval_array_abstract_object.h

@@ -32,7 +32,7 @@ class interval_array_abstract_objectt : public constant_array_abstract_objectt
     const index_exprt &index,
     const namespacet &ns) const override;
 
-  sharing_ptrt<array_abstract_objectt> write_index(
+  abstract_object_pointert write_index(
     abstract_environmentt &environment,
     const namespacet &ns,
     const std::stack<exprt> stack,

src/analyses/variable-sensitivity/value_set_array_abstract_object.cpp

@@ -42,7 +42,7 @@ abstract_object_pointert value_set_array_abstract_objectt::read_index(
   return array_abstract_objectt::read_index(env, index, ns);
 }
 
-sharing_ptrt<array_abstract_objectt>
+abstract_object_pointert
 value_set_array_abstract_objectt::write_index(
   abstract_environmentt &environment,
   const namespacet &ns,

src/analyses/variable-sensitivity/value_set_array_abstract_object.h

@@ -41,7 +41,7 @@ class value_set_array_abstract_objectt : public array_abstract_objectt
     const index_exprt &index,
     const namespacet &ns) const override;
 
-  sharing_ptrt<array_abstract_objectt> write_index(
+  abstract_object_pointert write_index(
     abstract_environmentt &environment,
     const namespacet &ns,
     std::stack<exprt> stack,