From 8f68057f665c5e6c89120598dd9773b39ae941e6 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 12 Apr 2019 21:34:48 +0000
Subject: [PATCH] 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.
---
 regression/cbmc/union13/main.c       | 12 ++++++++++++
 regression/cbmc/union13/no-arch.desc |  9 +++++++++
 regression/cbmc/union13/test.desc    |  8 ++++++++
 src/util/simplify_expr_int.cpp       | 17 ++++++++++++++++-
 4 files changed, 45 insertions(+), 1 deletion(-)
 create mode 100644 regression/cbmc/union13/main.c
 create mode 100644 regression/cbmc/union13/no-arch.desc
 create mode 100644 regression/cbmc/union13/test.desc

diff --git a/regression/cbmc/union13/main.c b/regression/cbmc/union13/main.c
new file mode 100644
index 00000000000..927bef371a7
--- /dev/null
+++ b/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);
+}
diff --git a/regression/cbmc/union13/no-arch.desc b/regression/cbmc/union13/no-arch.desc
new file mode 100644
index 00000000000..1e796102550
--- /dev/null
+++ b/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
diff --git a/regression/cbmc/union13/test.desc b/regression/cbmc/union13/test.desc
new file mode 100644
index 00000000000..9efefbc7362
--- /dev/null
+++ b/regression/cbmc/union13/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp
index fbf24059f2f..c0415b1c983 100644
--- a/src/util/simplify_expr_int.cpp
+++ b/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;
     }