Skip to content

Commit 21d1a61

Browse files
author
thk123
committed
Refactor member_of to make while loop clearer
1 parent fda0057 commit 21d1a61

File tree

1 file changed

+8
-11
lines changed

1 file changed

+8
-11
lines changed

jbmc/src/java_bytecode/java_bytecode_convert_method.cpp

Lines changed: 8 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -666,28 +666,25 @@ to_member(const exprt &pointer, const exprt &field_reference, const namespacet &
666666
const irep_idt &component_name = field_reference.get(ID_component_name);
667667

668668
exprt accessed_object = checked_dereference(typed_pointer, class_type);
669+
const auto type_of = [&ns](const exprt &object) {
670+
return to_struct_type(ns.follow(object.type()));
671+
};
669672

670673
// The field access is described as being against a particular type, but it
671674
// may in fact belong to any ancestor type.
672-
while(1)
675+
while(type_of(accessed_object).get_component(component_name).is_nil())
673676
{
674-
struct_typet object_type =
675-
to_struct_type(ns.follow(accessed_object.type()));
676-
auto component = object_type.get_component(component_name);
677-
678-
if(component.is_not_nil())
679-
return member_exprt(accessed_object, component);
680-
681-
// Component not present: check the immediate parent type.
682-
683-
const auto &components = object_type.components();
677+
const auto components = type_of(accessed_object).components();
684678
INVARIANT(
685679
components.size() != 0,
686680
"infer_opaque_type_fields should guarantee that a member access has a "
687681
"corresponding field");
688682

683+
// Base class access is always done through the first component
689684
accessed_object = member_exprt(accessed_object, components.front());
690685
}
686+
return member_exprt(
687+
accessed_object, type_of(accessed_object).get_component(component_name));
691688
}
692689

693690
/// Find all goto statements in 'repl' that target 'old_label' and redirect them

0 commit comments

Comments
 (0)