Add conversion of null pointer to smt terms

Author: thomasspriggs

src/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -6,6 +6,7 @@
 #include <util/c_types.h>
 #include <util/expr.h>
 #include <util/expr_cast.h>
+#include <util/expr_util.h>
 #include <util/floatbv_expr.h>
 #include <util/mathematical_expr.h>
 #include <util/pointer_expr.h>
@@ -268,6 +269,15 @@ struct sort_based_literal_convertert : public smt_sort_const_downcast_visitort
 
 static smt_termt convert_expr_to_smt(const constant_exprt &constant_literal)
 {
+  if(is_null_pointer(constant_literal))
+  {
+    const size_t bit_width =
+      type_checked_cast<pointer_typet>(constant_literal.type()).get_width();
+    // An address of 0 encodes an object identifier of 0 for the NULL object
+    // and an offset of 0 into the object.
+    const auto address = 0;
+    return smt_bit_vector_constant_termt{address, bit_width};
+  }
   const auto sort = convert_type_to_smt_sort(constant_literal.type());
   sort_based_literal_convertert converter(constant_literal);
   sort.accept(converter);

unit/solvers/smt2_incremental/convert_expr_to_smt.cpp

@@ -66,6 +66,24 @@ TEST_CASE(
       convert_expr_to_smt(from_integer({-1}, signedbv_typet{16})) ==
       smt_bit_vector_constant_termt{65535, 16});
   }
+  SECTION("Null pointer")
+  {
+    // These config lines are necessary because pointer widths depend on the
+    // configuration.
+    config.ansi_c.mode = configt::ansi_ct::flavourt::GCC;
+    config.ansi_c.set_arch_spec_i386();
+    const smt_termt null_pointer_term =
+      smt_bit_vector_constant_termt{0, config.ansi_c.pointer_width};
+    CHECK(
+      convert_expr_to_smt(null_pointer_exprt{pointer_type(void_type())}) ==
+      null_pointer_term);
+    CHECK(
+      convert_expr_to_smt(null_pointer_exprt{
+        pointer_type(unsignedbv_typet{100})}) == null_pointer_term);
+    CHECK(
+      convert_expr_to_smt(null_pointer_exprt{
+        pointer_type(pointer_type(void_type()))}) == null_pointer_term);
+  }
 }
 
 TEST_CASE(