expr2bits needs to handle pointer case

This fixes #4168. The pointer case was not handled.

Author: Daniel Kroening

regression/cbmc/assigning_nullpointers_should_not_crash_symex/main.c

@@ -1,5 +1,5 @@
 #include <assert.h>
-#include <stddef.h>
+#include <stdlib.h>
 
 struct linked_list
 {

regression/cbmc/assigning_nullpointers_should_not_crash_symex/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE broken-smt-backend
 main.c
 
 ^EXIT=0$

src/util/simplify_expr.cpp

@@ -1740,7 +1740,7 @@ optionalt<std::string> simplify_exprt::expr2bits(
     if(
       type.id() == ID_unsignedbv || type.id() == ID_signedbv ||
       type.id() == ID_floatbv || type.id() == ID_fixedbv ||
-      type.id() == ID_c_bit_field || type.id() == ID_pointer)
+      type.id() == ID_c_bit_field)
     {
       const auto width = to_bitvector_type(type).get_width();
 
@@ -1753,6 +1753,13 @@ optionalt<std::string> simplify_exprt::expr2bits(
 
       return result;
     }
+    else if(type.id() == ID_pointer)
+    {
+      if(value == ID_NULL && config.ansi_c.NULL_is_zero)
+        return std::string('0', to_bitvector_type(type).get_width());
+      else
+        return {};
+    }
     else if(type.id() == ID_c_enum_tag)
     {
       const auto &c_enum_type = ns.follow_tag(to_c_enum_tag_type(type));