Skip to content

Commit e13e090

Browse files
committed
Try to find a member-of expression instead of using byte-extract to retrieve substructures
1 parent 0a3f3ad commit e13e090

File tree

1 file changed

+9
-0
lines changed

1 file changed

+9
-0
lines changed

src/pointer-analysis/value_set_dereference.cpp

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -514,6 +514,8 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
514514
const typet &object_type=ns.follow(object.type());
515515
const exprt &root_object=o.root_object();
516516
const typet &root_object_type=ns.follow(root_object.type());
517+
518+
exprt root_object_subexpression=root_object;
517519

518520
if(dereference_type_compare(object_type, dereference_type) &&
519521
o.offset().is_zero())
@@ -573,6 +575,13 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
573575
if(ns.follow(result.value.type())!=ns.follow(dereference_type))
574576
result.value.make_typecast(dereference_type);
575577
}
578+
else if(get_subexpression_at_offset(root_object_subexpression, o.offset(),
579+
dereference_type, ns))
580+
{
581+
// Successfully found a member, array index, or combination thereof
582+
// that matches the desired type and offset:
583+
result.value=root_object_subexpression;
584+
}
576585
else
577586
{
578587
// we extract something from the root object

0 commit comments

Comments
 (0)