Merge pull request #4191 from tautschnig/byte-extract-pointers

byte_extract lowering of pointers [blocks: #2068]

Author: tautschnig

src/solvers/lowering/byte_operators.cpp

@@ -264,6 +264,17 @@ static exprt unpack_rec(
         member, little_endian, offset_bytes, max_bytes, ns, true);
     }
   }
+  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),