Skip to content

Commit a2cf16d

Browse files
Store symbol type instead of followed type when clean casting
Don't store followed type as type of superclass when doing clean cast as it may later change since we can now convert more methods after typechecking and doing this may change the type
1 parent f96efb4 commit a2cf16d

File tree

1 file changed

+7
-3
lines changed

1 file changed

+7
-3
lines changed

src/java_bytecode/java_pointer_casts.cpp

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -45,16 +45,20 @@ bool find_superclass_with_type(
4545
if(base_struct.components().empty())
4646
return false;
4747

48-
const typet &first_field_type=
49-
ns.follow(base_struct.components()[0].type());
48+
const typet &first_field_type=base_struct.components()[0].type();
5049
ptr=clean_deref(ptr);
50+
// Careful not to use the followed type here, as stub types may be
51+
// extended by later method conversion adding fields (e.g. an access
52+
// against x->y might add a new field `y` to the type of `*x`)
5153
ptr=member_exprt(
5254
ptr,
5355
base_struct.components()[0].get_name(),
5456
first_field_type);
5557
ptr=address_of_exprt(ptr);
5658

57-
if(first_field_type==target_type)
59+
// Compare the real (underlying) type, as target_type is already a non-
60+
// symbolic type.
61+
if(ns.follow(first_field_type)==target_type)
5862
return true;
5963
}
6064
}

0 commit comments

Comments
 (0)