diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp index 374fa6254a2..74299a6f2de 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp @@ -647,39 +647,46 @@ static irep_idt get_if_cmp_operator(const irep_idt &stmt) throw "unhandled java comparison instruction"; } -static member_exprt -to_member(const exprt &pointer, const exprt &fieldref, const namespacet &ns) +/// Build a member exprt for accessing a specific field that may come from a +/// base class. +/// \param pointer: The expression to access the field on. +/// \param field_reference: A getfield/setfield instruction produced by the +/// bytecode parser. +/// \param ns: Global namespace +/// \return A member expression accessing the field, through base class +/// components if necessary. +static member_exprt to_member( + const exprt &pointer, + const exprt &field_reference, + const namespacet &ns) { - struct_tag_typet class_type(fieldref.get(ID_class)); + struct_tag_typet class_type(field_reference.get(ID_class)); const exprt typed_pointer = typecast_exprt::conditional_cast(pointer, java_reference_type(class_type)); - const irep_idt &component_name = fieldref.get(ID_component_name); + const irep_idt &component_name = field_reference.get(ID_component_name); exprt accessed_object = checked_dereference(typed_pointer, class_type); + const auto type_of = [&ns](const exprt &object) { + return to_struct_type(ns.follow(object.type())); + }; // The field access is described as being against a particular type, but it // may in fact belong to any ancestor type. - while(1) + while(type_of(accessed_object).get_component(component_name).is_nil()) { - struct_typet object_type = - to_struct_type(ns.follow(accessed_object.type())); - auto component = object_type.get_component(component_name); - - if(component.is_not_nil()) - return member_exprt(accessed_object, component); - - // Component not present: check the immediate parent type. - - const auto &components = object_type.components(); + const auto components = type_of(accessed_object).components(); INVARIANT( components.size() != 0, "infer_opaque_type_fields should guarantee that a member access has a " "corresponding field"); + // Base class access is always done through the first component accessed_object = member_exprt(accessed_object, components.front()); } + return member_exprt( + accessed_object, type_of(accessed_object).get_component(component_name)); } /// Find all goto statements in 'repl' that target 'old_label' and redirect them diff --git a/src/goto-programs/remove_virtual_functions.cpp b/src/goto-programs/remove_virtual_functions.cpp index ec564b9c821..aa4863629c2 100644 --- a/src/goto-programs/remove_virtual_functions.cpp +++ b/src/goto-programs/remove_virtual_functions.cpp @@ -139,7 +139,7 @@ static void create_static_function_call( call_args[i].type().id() == ID_pointer, "where overriding function argument types differ, " "those arguments must be pointer-typed"); - call_args[i].make_typecast(need_type); + call_args[i] = typecast_exprt(call_args[i], need_type); } } }