Merge pull request #6781 from thomasspriggs/tas/smt_address_of

Add support for null pointer and address of expression conversion in incremental SMT2 backend.

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.

src/solvers/Makefile

@@ -195,6 +195,7 @@ SRC = $(BOOLEFORCE_SRC) \
       smt2/smt2irep.cpp \
       smt2_incremental/construct_value_expr_from_smt.cpp \
       smt2_incremental/convert_expr_to_smt.cpp \
+      smt2_incremental/object_tracking.cpp \
       smt2_incremental/smt_bit_vector_theory.cpp \
       smt2_incremental/smt_commands.cpp \
       smt2_incremental/smt_core_theory.cpp \