Bitvector decoding of pointer-typed constants must use bvrep

The regression test demonstrated that decoding non-null pointer-typed
constants were not correctly decoded to their integer representation.

Author: tautschnig

regression/goto-instrument/dump-union/main.c

@@ -1,8 +1,11 @@
+#include <assert.h>
+
 union U {
   int *p;
   unsigned long long p_int;
 } u = {.p_int = 42};
 
 int main()
 {
+  assert(u.p_int == 42);
 }

regression/goto-instrument/dump-union/test.desc

@@ -2,6 +2,7 @@ CORE
 main.c
 --dump-c
 =(\(signed int \*\))?42
+VERIFICATION SUCCESSFUL
 ^EXIT=0$
 ^SIGNAL=0$
 --

src/solvers/flattening/bv_pointers.cpp

@@ -308,7 +308,7 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
       encode(pointer_logic.get_null_object(), bv);
     else
     {
-      mp_integer i=string2integer(id2string(value), 2);
+      mp_integer i = bvrep2integer(value, bits, false);
       bv=bv_utils.build_constant(i, bits);
     }