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.
This commit is contained in:
parent
7632d0276e
commit
004bd27a49
|
@ -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
|
||||
|
|
|
@ -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),
|
||||
|
|
Loading…
Reference in New Issue