NULL compares equal to 0

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,11 @@
+#include <assert.h>
+
+int main()
+{
+  union {
+    unsigned long long i;
+    int *p;
+  } u;
+  u.i = 0;
+  assert(u.p == 0);
+}

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,13 @@ bool simplify_exprt::simplify_inequality(exprt &expr)
   {
     if(expr.id() == ID_equal || expr.id() == ID_notequal)
     {
-
-      bool equal = (tmp0_const->get_value() == tmp1_const->get_value());
+      // 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
+      const bool equal =
+        (tmp0_const->get_value() == tmp1_const->get_value()) ||
+        (tmp0_const->type().id() == ID_pointer &&
+         tmp1_const->type().id() == ID_pointer && config.ansi_c.NULL_is_zero &&
+         tmp0_const->is_zero() && tmp1_const->is_zero());
       expr.make_bool(expr.id() == ID_equal ? equal : !equal);
       return false;
     }