Null-pointer filtering must handle unknown offsets

A non-constant offset is stored as "unknown," which does include an
offset of zero. As constant + zero == constant we should not conclude
that the constant is not contained in the set.

Author: tautschnig

regression/cbmc/null7/main.c

@@ -0,0 +1,28 @@
+#include <stdlib.h>
+
+_Bool nondet_bool();
+
+int main()
+{
+  char *s = NULL;
+  char A[3];
+  _Bool s_is_set = 0;
+
+  if(nondet_bool())
+  {
+    s = A;
+    s_is_set = 1;
+  }
+
+  if(s_is_set)
+  {
+    unsigned len;
+    __CPROVER_assume(len < 3);
+    s += len;
+  }
+
+  if(s)
+    *s = 42;
+
+  return 0;
+}

regression/cbmc/null7/test.desc

@@ -0,0 +1,11 @@
+CORE broken-smt-backend
+main.c
+--pointer-check
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
+--
+The value set may contain the constants with unknown offsets. Such cases cannot
+be conclusively filtered out as the offset may be zero.

src/goto-symex/symex_goto.cpp

@@ -114,7 +114,8 @@ static optionalt<renamedt<exprt, L2>> try_evaluate_pointer_comparison(
       value_set_element.id() == ID_unknown ||
       value_set_element.id() == ID_invalid ||
       is_failed_symbol(
-        to_object_descriptor_expr(value_set_element).root_object()))
+        to_object_descriptor_expr(value_set_element).root_object()) ||
+      to_object_descriptor_expr(value_set_element).offset().id() == ID_unknown)
     {
       // We can't conclude anything about the value-set
       return {};