Merge pull request #6142 from tautschnig/pointer-comparison-simplify

simplify_inequality_address_of only supports (not)equal

Author: tautschnig

regression/cbmc/Pointer_comparison3/main.c

@@ -0,0 +1,9 @@
+#include <assert.h>
+#include <stdlib.h>
+
+int main()
+{
+  int *p1 = malloc(sizeof(int));
+
+  assert(p1 < p1 + 1);
+}

regression/cbmc/Pointer_comparison3/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

src/util/simplify_expr_int.cpp

@@ -1242,7 +1242,8 @@ simplify_exprt::simplify_inequality(const binary_relation_exprt &expr)
   // see if we are comparing pointers that are address_of
   if(
     skip_typecast(tmp0).id() == ID_address_of &&
-    skip_typecast(tmp1).id() == ID_address_of)
+    skip_typecast(tmp1).id() == ID_address_of &&
+    (expr.id() == ID_equal || expr.id() == ID_notequal))
   {
     return simplify_inequality_address_of(expr);
   }