byte_extract lowering of pointers

Bit operations cannot be performed on pointers, thus type cast them to unsigned
bitvectors first and then convert back the result.

Author: tautschnig

src/solvers/lowering/byte_operators.cpp

@@ -236,6 +236,17 @@ static exprt unpack_rec(
       std::move(byte_operands),
       array_typet(unsignedbv_typet(8), from_integer(size, size_type())));
   }
+  else if(src.type().id() == ID_pointer)
+  {
+    return unpack_rec(
+      typecast_exprt(
+        src, unsignedbv_typet(to_pointer_type(src.type()).get_width())),
+      little_endian,
+      offset_bytes,
+      max_bytes,
+      ns,
+      unpack_byte_array);
+  }
   else if(src.type().id()!=ID_empty)
   {
     // a basic type; we turn that into extractbits while considering

unit/solvers/lowering/byte_operators.cpp

@@ -124,6 +124,7 @@ SCENARIO("byte_extract_lowering", "[core][solvers][lowering][byte_extract]")
       signedbv_typet(24),
       signedbv_typet(128),
       // ieee_float_spect::single_precision().to_type(),
+      // generates the correct value, but remains wrapped in a typecast
       // pointer_typet(u64, 64),
       vector_typet(u8, size),
       vector_typet(u64, size),