diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp index 571d8bd0ad1..110ed0b8f7c 100644 --- a/src/analyses/goto_rw.cpp +++ b/src/analyses/goto_rw.cpp @@ -221,12 +221,12 @@ void rw_range_sett::get_objects_member( const struct_typet &struct_type=to_struct_type(type); - // TODO - assumes members are byte-aligned range_spect offset= - to_range_spect(member_offset( + to_range_spect( + member_offset_bits( struct_type, expr.get_component_name(), - ns) * 8); + ns)); if(offset!=-1) offset+=range_start; diff --git a/src/util/pointer_offset_size.cpp b/src/util/pointer_offset_size.cpp index dee9aeff82d..798266792eb 100644 --- a/src/util/pointer_offset_size.cpp +++ b/src/util/pointer_offset_size.cpp @@ -80,6 +80,29 @@ mp_integer member_offset( return offsets->second; } +mp_integer member_offset_bits( + const struct_typet &type, + const irep_idt &member, + const namespacet &ns) +{ + mp_integer offset=0; + const struct_typet::componentst &components=type.components(); + + for(const auto &comp : components) + { + if(comp.get_name()==member) + break; + + mp_integer member_bits=pointer_offset_bits(comp.type(), ns); + if(member_bits==-1) + return member_bits; + + offset+=member_bits; + } + + return offset; +} + mp_integer pointer_offset_size( const typet &type, const namespacet &ns) diff --git a/src/util/pointer_offset_size.h b/src/util/pointer_offset_size.h index aeb62e03d74..0bdd67f85d3 100644 --- a/src/util/pointer_offset_size.h +++ b/src/util/pointer_offset_size.h @@ -45,6 +45,11 @@ mp_integer member_offset( const irep_idt &member, const namespacet &ns); +mp_integer member_offset_bits( + const struct_typet &type, + const irep_idt &member, + const namespacet &ns); + mp_integer pointer_offset_size( const typet &type, const namespacet &ns);