@@ -628,38 +628,36 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
628628 }
629629 }
630630
631+ // try to build a member/index expression - do not use byte_extract
632+ auto subexpr = get_subexpression_at_offset (
633+ root_object_subexpression, o.offset (), dereference_type, ns);
634+ if (subexpr.has_value ())
635+ simplify (subexpr.value (), ns);
636+ if (
637+ subexpr.has_value () &&
638+ subexpr.value ().id () != ID_byte_extract_little_endian &&
639+ subexpr.value ().id () != ID_byte_extract_big_endian)
631640 {
632- // try to build a member/index expression - do not use byte_extract
633- auto subexpr = get_subexpression_at_offset (
634- root_object_subexpression, o.offset (), dereference_type, ns);
635- if (subexpr.has_value ())
636- simplify (subexpr.value (), ns);
637- if (
638- subexpr.has_value () &&
639- subexpr.value ().id () != ID_byte_extract_little_endian &&
640- subexpr.value ().id () != ID_byte_extract_big_endian)
641- {
642- // Successfully found a member, array index, or combination thereof
643- // that matches the desired type and offset:
644- result.value = subexpr.value ();
645- result.pointer = typecast_exprt::conditional_cast (
646- address_of_exprt{skip_typecast (subexpr.value ())}, pointer_type);
647- return result;
648- }
649-
650- // we extract something from the root object
651- result.value =o.root_object ();
641+ // Successfully found a member, array index, or combination thereof
642+ // that matches the desired type and offset:
643+ result.value = subexpr.value ();
652644 result.pointer = typecast_exprt::conditional_cast (
653- address_of_exprt{skip_typecast (o.root_object ())}, pointer_type);
645+ address_of_exprt{skip_typecast (subexpr.value ())}, pointer_type);
646+ return result;
647+ }
654648
655- if (memory_model (result.value , dereference_type, offset, ns))
656- {
657- // ok, done
658- }
659- else
660- {
661- return valuet (); // give up, no way that this is ok
662- }
649+ // we extract something from the root object
650+ result.value = o.root_object ();
651+ result.pointer = typecast_exprt::conditional_cast (
652+ address_of_exprt{skip_typecast (o.root_object ())}, pointer_type);
653+
654+ if (memory_model (result.value , dereference_type, offset, ns))
655+ {
656+ // ok, done
657+ }
658+ else
659+ {
660+ return valuet (); // give up, no way that this is ok
663661 }
664662 }
665663
0 commit comments