We never call write on an abstract_value_objectt.

Consequently we can remove value_set_abstract_objectt::write and
value_set_*::resolve_new_values.

Added UNREACHABLE assertion in abstract_value_objectt::write should this
every change (deliverately or otherwise).

Author: jezhiggins

src/analyses/variable-sensitivity/abstract_value_object.cpp

@@ -177,6 +177,17 @@ abstract_object_pointert abstract_value_objectt::expression_transform(
   return environment.add_object_context(result);
 }
 
+abstract_object_pointert abstract_value_objectt::write(
+  abstract_environmentt &environment,
+  const namespacet &ns,
+  const std::stack<exprt> &stack,
+  const exprt &specifier,
+  const abstract_object_pointert &value,
+  bool merging_write) const
+{
+  UNREACHABLE; // Should not ever call write on a value;
+}
+
 abstract_object_pointert abstract_value_objectt::merge(
   const abstract_object_pointert &other,
   const wident &widen_mode) const

src/analyses/variable-sensitivity/abstract_value_object.h

@@ -286,6 +286,14 @@ class abstract_value_objectt : public abstract_objectt,
     const abstract_environmentt &environment,
     const namespacet &ns) const final;
 
+  abstract_object_pointert write(
+    abstract_environmentt &environment,
+    const namespacet &ns,
+    const std::stack<exprt> &stack,
+    const exprt &specifier,
+    const abstract_object_pointert &value,
+    bool merging_write) const final;
+
 protected:
   using abstract_value_pointert = sharing_ptrt<const abstract_value_objectt>;
 

src/analyses/variable-sensitivity/value_set_abstract_object.cpp

@@ -182,23 +182,6 @@ constant_interval_exprt value_set_abstract_objectt::to_interval() const
   return values.to_interval();
 }
 
-abstract_object_pointert value_set_abstract_objectt::write(
-  abstract_environmentt &environment,
-  const namespacet &ns,
-  const std::stack<exprt> &stack,
-  const exprt &specifier,
-  const abstract_object_pointert &value,
-  bool merging_write) const
-{
-  abstract_object_sett new_values;
-  for(const auto &st_value : values)
-  {
-    new_values.insert(
-      st_value->write(environment, ns, stack, specifier, value, merging_write));
-  }
-  return resolve_new_values(new_values, environment);
-}
-
 abstract_object_pointert value_set_abstract_objectt::merge_with_value(
   const abstract_value_pointert &other,
   const wident &widen_mode) const
@@ -252,14 +235,6 @@ abstract_object_pointert value_set_abstract_objectt::meet_with_value(
   return resolve_values(meet_values);
 }
 
-abstract_object_pointert value_set_abstract_objectt::resolve_new_values(
-  const abstract_object_sett &new_values,
-  const abstract_environmentt &environment) const
-{
-  auto result = resolve_values(new_values);
-  return environment.add_object_context(result);
-}
-
 abstract_object_pointert value_set_abstract_objectt::resolve_values(
   const abstract_object_sett &new_values) const
 {

src/analyses/variable-sensitivity/value_set_abstract_object.h

@@ -54,17 +54,6 @@ class value_set_abstract_objectt : public abstract_value_objectt,
   /// either converted to interval or marked as `top`.
   static const size_t max_value_set_size = 10;
 
-  /// \copydoc abstract_objectt::write
-  ///
-  /// Delegate writing to stored values.
-  abstract_object_pointert write(
-    abstract_environmentt &environment,
-    const namespacet &ns,
-    const std::stack<exprt> &stack,
-    const exprt &specifier,
-    const abstract_object_pointert &value,
-    bool merging_write) const override;
-
   void output(std::ostream &out, const ai_baset &ai, const namespacet &ns)
     const override;
 
@@ -79,16 +68,6 @@ class value_set_abstract_objectt : public abstract_value_objectt,
   meet_with_value(const abstract_value_pointert &other) const override;
 
 private:
-  /// Update the set of stored values to \p new_values. Build a new abstract
-  ///   object of the right type if necessary.
-  /// \param new_values: potentially new set of values
-  /// \param environment: the abstract environment
-  /// \return the abstract object representing \p new_values (either 'this' or
-  ///   something new)
-  abstract_object_pointert resolve_new_values(
-    const abstract_object_sett &new_values,
-    const abstract_environmentt &environment) const;
-
   /// Update the set of stored values to \p new_values. Build a new abstract
   ///   object of the right type if necessary.
   /// \param new_values: potentially new set of values

src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp

@@ -139,14 +139,6 @@ abstract_object_pointert value_set_pointer_abstract_objectt::write_dereference(
   return shared_from_this();
 }
 
-abstract_object_pointert value_set_pointer_abstract_objectt::resolve_new_values(
-  const abstract_object_sett &new_values,
-  const abstract_environmentt &environment) const
-{
-  auto result = resolve_values(new_values);
-  return environment.add_object_context(result);
-}
-
 abstract_object_pointert value_set_pointer_abstract_objectt::resolve_values(
   const abstract_object_sett &new_values) const
 {

src/analyses/variable-sensitivity/value_set_pointer_abstract_object.h

@@ -76,16 +76,6 @@ class value_set_pointer_abstract_objectt : public abstract_pointer_objectt,
     const wident &widen_mode) const override;
 
 private:
-  /// Update the set of stored values to \p new_values. Build a new abstract
-  ///   object of the right type if necessary.
-  /// \param new_values: potentially new set of values
-  /// \param environment: the abstract environment
-  /// \return the abstract object representing \p new_values (either 'this' or
-  ///   something new)
-  abstract_object_pointert resolve_new_values(
-    const abstract_object_sett &new_values,
-    const abstract_environmentt &environment) const;
-
   /// Update the set of stored values to \p new_values. Build a new abstract
   ///   object of the right type if necessary.
   /// \param new_values: potentially new set of values