Simply pointer_abstract_objectt::write_dereference

Author: jezhiggins

src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp

@@ -169,7 +169,7 @@ abstract_object_pointert constant_pointer_abstract_objectt::read_dereference(
   }
 }
 
-sharing_ptrt<pointer_abstract_objectt>
+abstract_object_pointert
 constant_pointer_abstract_objectt::write_dereference(
   abstract_environmentt &environment,
   const namespacet &ns,

src/analyses/variable-sensitivity/constant_pointer_abstract_object.h

@@ -99,7 +99,7 @@ class constant_pointer_abstract_objectt : public pointer_abstract_objectt
   ///
   /// \return A modified abstract object representing this pointer after it
   ///         has been written to.
-  sharing_ptrt<pointer_abstract_objectt> write_dereference(
+  abstract_object_pointert write_dereference(
     abstract_environmentt &environment,
     const namespacet &ns,
     const std::stack<exprt> stack,

src/analyses/variable-sensitivity/pointer_abstract_object.cpp

@@ -65,7 +65,9 @@ abstract_object_pointert pointer_abstract_objectt::read_dereference(
   return env.abstract_object_factory(pointed_to_type, ns, true, false);
 }
 
-sharing_ptrt<pointer_abstract_objectt>
+#include <iostream>
+
+abstract_object_pointert
 pointer_abstract_objectt::write_dereference(
   abstract_environmentt &environment,
   const namespacet &ns,
@@ -76,12 +78,11 @@ pointer_abstract_objectt::write_dereference(
   if(is_top() || is_bottom())
   {
     environment.havoc("Writing to a 2value pointer");
-    return std::dynamic_pointer_cast<const pointer_abstract_objectt>(clone());
+    return shared_from_this();
   }
   else
   {
-    return sharing_ptrt<pointer_abstract_objectt>(
-      new pointer_abstract_objectt(type(), true, false));
+    return std::make_shared<pointer_abstract_objectt>(type(), true, false);
   }
 }
 

src/analyses/variable-sensitivity/pointer_abstract_object.h

@@ -120,7 +120,7 @@ class pointer_abstract_objectt : public abstract_objectt
   ///
   /// \return A modified abstract object representing this pointer after it
   ///         has been written to.
-  virtual sharing_ptrt<pointer_abstract_objectt> write_dereference(
+  virtual abstract_object_pointert write_dereference(
     abstract_environmentt &environment,
     const namespacet &ns,
     const std::stack<exprt> stack,

src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp

@@ -47,7 +47,7 @@ abstract_object_pointert value_set_pointer_abstract_objectt::read_dereference(
   return pointer_abstract_objectt::read_dereference(env, ns);
 }
 
-sharing_ptrt<pointer_abstract_objectt>
+abstract_object_pointert
 value_set_pointer_abstract_objectt::write_dereference(
   abstract_environmentt &environment,
   const namespacet &ns,

src/analyses/variable-sensitivity/value_set_pointer_abstract_object.h

@@ -42,7 +42,7 @@ class value_set_pointer_abstract_objectt : public pointer_abstract_objectt
     const abstract_environmentt &env,
     const namespacet &ns) const override;
 
-  sharing_ptrt<pointer_abstract_objectt> write_dereference(
+  abstract_object_pointert write_dereference(
     abstract_environmentt &environment,
     const namespacet &ns,
     std::stack<exprt> stack,