Add incremental smt2 with null pointers regression test

Author: thomasspriggs

regression/cbmc-incr-smt2/pointers/null_pointer.c

@@ -0,0 +1,21 @@
+#include <assert.h>
+#include <inttypes.h>
+#include <stdbool.h>
+#include <stddef.h>
+
+int main()
+{
+  int notdet_int;
+  int *ptr;
+  bool notdet_bool;
+  if(notdet_bool)
+  {
+    ptr = &notdet_int;
+    assert(((uint64_t)ptr) > 1);
+  }
+  else
+  {
+    ptr = NULL;
+  }
+  assert(((uint64_t)ptr) != 0);
+}

regression/cbmc-incr-smt2/pointers/null_pointer.desc

@@ -0,0 +1,17 @@
+CORE
+null_pointer.c
+--trace
+Passing problem to incremental SMT2 solving
+line 14 assertion \(\(uint64_t\)ptr\) > 1: SUCCESS
+line 20 assertion \(\(uint64_t\)ptr\) != 0: FAILURE
+notdet_bool=FALSE \(0+\)
+^EXIT=10$
+^SIGNAL=0$
+--
+notdet_bool=TRUE
+--
+Tests for null related functionality.
+ * Assignment of the value NULL to a pointer.
+ * Comparison of NULL pointer value against 0.
+ * Check that the address of a non-null pointer is not an offset into the NULL
+   object.