Remove ptr_diff_exprt

Detect case by checking expr has ID_minus and the operands are both
pointers.

Author: jezhiggins

src/analyses/variable-sensitivity/abstract_environment.cpp

@@ -54,6 +54,11 @@ std::vector<abstract_object_pointert> eval_operands(
   const abstract_environmentt &env,
   const namespacet &ns);
 
+static bool is_ptr_diff(const exprt& expr) {
+  return (expr.id() == ID_minus) &&
+         (expr.operands()[0].type().id() == ID_pointer) &&
+         (expr.operands()[1].type().id() == ID_pointer);
+}
 exprt simplify_vsd_expr(exprt src, const namespacet &ns);
 
 abstract_object_pointert
@@ -71,7 +76,7 @@ abstract_environmentt::eval(const exprt &expr, const namespacet &ns) const
 
   if(
     simplified_id == ID_member || simplified_id == ID_index ||
-    simplified_id == ID_dereference || simplified_id == ID_ptr_diff)
+    simplified_id == ID_dereference || is_ptr_diff(simplified_expr))
   {
     auto access_expr = simplified_expr;
     auto target = eval(access_expr.operands()[0], ns);

src/analyses/variable-sensitivity/abstract_pointer_object.cpp

@@ -37,6 +37,11 @@ abstract_pointer_objectt::abstract_pointer_objectt(
   PRECONDITION(e.type().id() == ID_pointer);
 }
 
+static bool is_ptr_diff(const exprt& expr) {
+  return (expr.id() == ID_minus) &&
+         (expr.operands()[1].type().id() == ID_pointer);
+}
+
 abstract_object_pointert abstract_pointer_objectt::expression_transform(
   const exprt &expr,
   const std::vector<abstract_object_pointert> &operands,
@@ -46,7 +51,7 @@ abstract_object_pointert abstract_pointer_objectt::expression_transform(
   if(expr.id() == ID_dereference)
     return read_dereference(environment, ns);
 
-  if(expr.id() == ID_ptr_diff)
+  if(is_ptr_diff(expr))
   {
     auto &rhs = operands[1];
     if(same_target(rhs))

src/util/irep_ids.def

@@ -861,7 +861,6 @@ IREP_ID_TWO(vector_gt, vector->)
 IREP_ID_TWO(vector_lt, vector-<)
 IREP_ID_ONE(shuffle_vector)
 IREP_ID_ONE(count_trailing_zeros)
-IREP_ID_ONE(ptr_diff)
 
 // Projects depending on this code base that wish to extend the list of
 // available ids should provide a file local_irep_ids.def in their source tree

src/util/std_expr.h

@@ -928,26 +928,6 @@ inline minus_exprt &to_minus_expr(exprt &expr)
   return ret;
 }
 
-class ptr_diff_exprt : public expr_protectedt
-{
-private:
-  ptr_diff_exprt(const minus_exprt &minus_expr)
-    : expr_protectedt(ID_ptr_diff, minus_expr.type(), minus_expr.operands())
-  {
-    PRECONDITION(op0().type().id() == ID_pointer);
-    PRECONDITION(op1().type().id() == ID_pointer);
-  }
-
-  friend ptr_diff_exprt to_ptr_diff_expr(const minus_exprt &expr);
-};
-
-inline ptr_diff_exprt to_ptr_diff_expr(const minus_exprt &expr)
-{
-  PRECONDITION(expr.lhs().type().id() == ID_pointer);
-  PRECONDITION(expr.rhs().type().id() == ID_pointer);
-  return ptr_diff_exprt(expr);
-}
-
 /// \brief Binary multiplication
 /// Associativity is not specified.
 class mult_exprt:public multi_ary_exprt