NULL compares equal to 0 when config.ansi_c.NULL_is_zero is set

When comparing constants, we just compared their string representations.
This fails when one side of the (in)equality was NULL while the other
side was 0, which is wrong when config.ansi_c.NULL_is_zero is set. Thus
actually test both sides for being zero in this configuration.

Author: tautschnig

regression/cbmc/union13/main.c

@@ -0,0 +1,12 @@
+#include <assert.h>
+#include <stdint.h>
+
+int main()
+{
+  union {
+    intptr_t i;
+    int *p;
+  } u;
+  u.i = 0;
+  assert(u.p == 0);
+}

regression/cbmc/union13/no-arch.desc

@@ -0,0 +1,9 @@
+CORE broken-smt-backend
+main.c
+--arch none --little-endian
+(Starting CEGAR Loop|^Generated 1 VCC\(s\), 1 remaining after simplification$)
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

regression/cbmc/union13/test.desc

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

src/util/simplify_expr_int.cpp

@@ -1357,8 +1357,23 @@ bool simplify_exprt::simplify_inequality(exprt &expr)
   {
     if(expr.id() == ID_equal || expr.id() == ID_notequal)
     {
-
+      // two constants compare equal when there values (as strings) are the same
+      // or both of them are pointers and both represent NULL in some way
       bool equal = (tmp0_const->get_value() == tmp1_const->get_value());
+      if(
+        !equal && tmp0_const->type().id() == ID_pointer &&
+        tmp1_const->type().id() == ID_pointer)
+      {
+        if(
+          !config.ansi_c.NULL_is_zero && (tmp0_const->get_value() == ID_NULL ||
+                                          tmp1_const->get_value() == ID_NULL))
+        {
+          // if NULL is not zero on this platform, we really don't know what it
+          // is and therefore cannot simplify
+          return true;
+        }
+        equal = tmp0_const->is_zero() && tmp1_const->is_zero();
+      }
       expr.make_bool(expr.id() == ID_equal ? equal : !equal);
       return false;
     }