let inverted pointer expression eval as normal. No need for special case.

Author: jezhiggins

regression/goto-analyzer/pointer-comparison-equality-same-target-2/main.c

@@ -0,0 +1,16 @@
+#include <assert.h>
+
+int main()
+{
+  int a[2];
+
+  int *p = &(a[0]);
+  int *q = &(a[1]);
+  int *r = p + 1;
+
+  assert(p == q || p == r);
+  assert(q == p || q == r);
+
+  assert(p != q && p != r);
+  assert(q != p && q != r);
+}

regression/goto-analyzer/pointer-comparison-equality-same-target-2/test-constants.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--variable-sensitivity --vsd-pointers constants --verify
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] .* assertion p == q || p == r: FAILURE
+^\[main.assertion.2\] .* assertion q == p || q == r: SUCCESS
+^\[main.assertion.3\] .* assertion p != q && p != r: SUCCESS
+^\[main.assertion.4\] .* assertion q != p && q != r: FAILURE

regression/goto-analyzer/pointer-comparison-equality-same-target-2/test-top-bottom.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--variable-sensitivity --vsd-pointers top-bottom --verify
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] .* assertion p == q || p == r: UNKNOWN
+^\[main.assertion.2\] .* assertion q == p || q == r: UNKNOWN
+^\[main.assertion.3\] .* assertion p != q && p != r: UNKNOWN
+^\[main.assertion.4\] .* assertion q != p && q != r: UNKNOWN

regression/goto-analyzer/pointer-comparison-equality-same-target-2/test-value-set.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--variable-sensitivity --vsd-pointers value-set --verify
+^EXIT=0$
+^SIGNAL=0$
+^\[main.assertion.1\] .* assertion p == q || p == r: FAILURE
+^\[main.assertion.2\] .* assertion q == p || q == r: SUCCESS
+^\[main.assertion.3\] .* assertion p != q && p != r: SUCCESS
+^\[main.assertion.4\] .* assertion q != p && q != r: FAILURE

src/analyses/variable-sensitivity/abstract_environment.cpp

@@ -46,8 +46,8 @@ static exprt assume_greater_than(
   const exprt &expr,
   const namespacet &ns);
 
-abstract_value_pointert as_value(const abstract_object_pointert &obj);
-bool is_value(const abstract_object_pointert &obj);
+static abstract_value_pointert as_value(const abstract_object_pointert &obj);
+static bool is_value(const abstract_object_pointert &obj);
 
 std::vector<abstract_object_pointert> eval_operands(
   const exprt &expr,
@@ -64,12 +64,6 @@ bool is_ptr_diff(const exprt &expr)
 bool is_ptr_comparison(const exprt &expr)
 {
   auto const &id = expr.id();
-  if(id == ID_not)
-  {
-    auto const &not_expr = to_not_expr(expr);
-    return is_ptr_comparison(not_expr.op());
-  }
-
   bool is_comparison = id == ID_equal || id == ID_notequal || id == ID_lt ||
                        id == ID_le || id == ID_gt || id == ID_ge;
 
@@ -110,10 +104,7 @@ abstract_environmentt::eval(const exprt &expr, const namespacet &ns) const
     is_access_expr(simplified_id) || is_ptr_diff(simplified_expr) ||
     is_ptr_comparison(simplified_expr))
   {
-    auto const &operands_expr = (simplified_id != ID_not)
-                                  ? simplified_expr
-                                  : to_not_expr(simplified_expr).op();
-    auto const operands = eval_operands(operands_expr, *this, ns);
+    auto const operands = eval_operands(simplified_expr, *this, ns);
     auto const &target = operands.front();
 
     return target->expression_transform(simplified_expr, operands, *this, ns);
@@ -560,7 +551,7 @@ static auto inverse_operations =
                                {ID_ge, ID_lt},
                                {ID_gt, ID_le}};
 
-exprt invert_result(const exprt &result)
+static exprt invert_result(const exprt &result)
 {
   if(!result.is_boolean())
     return result;
@@ -570,7 +561,7 @@ exprt invert_result(const exprt &result)
   return true_exprt();
 }
 
-exprt invert_expr(const exprt &expr)
+static exprt invert_expr(const exprt &expr)
 {
   auto expr_id = expr.id();
 

src/analyses/variable-sensitivity/abstract_environment.h

@@ -22,7 +22,6 @@
 #include <analyses/variable-sensitivity/abstract_object.h>
 
 exprt simplify_vsd_expr(exprt src, const namespacet &ns);
-exprt invert_result(const exprt &result);
 bool is_ptr_diff(const exprt &expr);
 bool is_ptr_comparison(const exprt &expr);
 

src/analyses/variable-sensitivity/abstract_pointer_object.cpp

@@ -116,26 +116,10 @@ abstract_object_pointert abstract_pointer_objectt::eval_ptr_comparison(
   const abstract_environmentt &environment,
   const namespacet &ns) const
 {
-  auto result = eval_ptr_comparison_as_expr(expr, operands, environment, ns);
+  auto result = ptr_comparison_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,11 +129,6 @@ 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/context_abstract_object.cpp

@@ -86,6 +86,7 @@ abstract_object_pointert context_abstract_objectt::expression_transform(
   const abstract_environmentt &environment,
   const namespacet &ns) const
 {
+  PRECONDITION(expr.operands().size() == operands.size());
   std::vector<abstract_object_pointert> child_operands;
 
   std::transform(