Remove duplication in ptr_comparison_expr

Author: jezhiggins

src/analyses/variable-sensitivity/abstract_pointer_object.cpp

@@ -116,10 +116,26 @@ abstract_object_pointert abstract_pointer_objectt::eval_ptr_comparison(
   const abstract_environmentt &environment,
   const namespacet &ns) const
 {
-  auto result = ptr_comparison_expr(expr, operands, environment, ns);
+  auto result = eval_ptr_comparison_as_expr(expr, operands, environment, ns);
   return environment.eval(result, ns);
 }
 
+exprt abstract_pointer_objectt::eval_ptr_comparison_as_expr(
+  const exprt &expr,
+  const std::vector<abstract_object_pointert> &operands,
+  const abstract_environmentt &environment,
+  const namespacet &ns) const
+{
+  if(expr.id() == ID_not)
+  {
+    auto const &not_expr = to_not_expr(expr);
+    auto result = simplify_vsd_expr(
+      ptr_comparison_expr(not_expr.op(), operands, environment, ns), ns);
+    return invert_result(result);
+  }
+  return ptr_comparison_expr(expr, operands, environment, ns);
+}
+
 static bool is_dereference(const exprt &expr)
 {
   return expr.id() == ID_dereference;

src/analyses/variable-sensitivity/abstract_pointer_object.h

@@ -129,6 +129,11 @@ class abstract_pointer_objectt : public abstract_objectt,
     const std::vector<abstract_object_pointert> &operands,
     const abstract_environmentt &environment,
     const namespacet &ns) const;
+  exprt eval_ptr_comparison_as_expr(
+    const exprt &expr,
+    const std::vector<abstract_object_pointert> &operands,
+    const abstract_environmentt &environment,
+    const namespacet &ns) const;
 };
 
 #endif // CPROVER_ANALYSES_VARIABLE_SENSITIVITY_ABSTRACT_POINTER_OBJECT_H

src/analyses/variable-sensitivity/constant_pointer_abstract_object.cpp

@@ -361,14 +361,6 @@ exprt constant_pointer_abstract_objectt::ptr_comparison_expr(
   const abstract_environmentt &environment,
   const namespacet &ns) const
 {
-  if(expr.id() == ID_not)
-  {
-    auto const &not_expr = to_not_expr(expr);
-    auto result = simplify_vsd_expr(
-      ptr_comparison_expr(not_expr.op(), operands, environment, ns), ns);
-    return invert_result(result);
-  }
-
   auto rhs = std::dynamic_pointer_cast<const constant_pointer_abstract_objectt>(
     operands.back());
 

src/analyses/variable-sensitivity/value_set_pointer_abstract_object.cpp

@@ -166,14 +166,6 @@ exprt value_set_pointer_abstract_objectt::ptr_comparison_expr(
   const abstract_environmentt &environment,
   const namespacet &ns) const
 {
-  if(expr.id() == ID_not)
-  {
-    auto const &not_expr = to_not_expr(expr);
-    auto result = simplify_vsd_expr(
-      ptr_comparison_expr(not_expr.op(), operands, environment, ns), ns);
-    return invert_result(result);
-  }
-
   auto rhs =
     std::dynamic_pointer_cast<const value_set_pointer_abstract_objectt>(
       operands.back());