Skip to content

Commit 5b885d6

Browse files
author
thk123
committed
Refactor member_of to make while loop clearer
1 parent 6a02889 commit 5b885d6

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
@@ -668,28 +668,25 @@ static member_exprt to_member(
668668
const irep_idt &component_name = field_reference.get(ID_component_name);
669669

670670
exprt accessed_object = checked_dereference(typed_pointer, class_type);
671+
const auto type_of = [&ns](const exprt &object) {
672+
return to_struct_type(ns.follow(object.type()));
673+
};
671674

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

685+
// Base class access is always done through the first component
691686
accessed_object = member_exprt(accessed_object, components.front());
692687
}
688+
return member_exprt(
689+
accessed_object, type_of(accessed_object).get_component(component_name));
693690
}
694691

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

0 commit comments

Comments
 (0)