Skip to content

Commit c07e6ca

Browse files
author
svorenova
committed
Update generic specialization map when replacing pointers
When initiliazing a pointer and it is replaced by a different pointer due to inheritence make sure that the generic parameter specialization map is updated too.
1 parent da63652 commit c07e6ca

File tree

1 file changed

+7
-0
lines changed

1 file changed

+7
-0
lines changed

src/java_bytecode/java_object_factory.cpp

+7
Original file line numberDiff line numberDiff line change
@@ -766,6 +766,13 @@ void java_object_factoryt::gen_nondet_pointer_init(
766766
// for java types, technical debt TG-2707
767767
if(!equal_java_types(replacement_pointer_type, pointer_type))
768768
{
769+
// update generic_parameter_specialization_map for the new pointer
770+
generic_parameter_specialization_map_keyst
771+
generic_parameter_specialization_map_keys(
772+
generic_parameter_specialization_map);
773+
generic_parameter_specialization_map_keys.insert_pairs_for_pointer(
774+
replacement_pointer_type, ns.follow(replacement_pointer_type.subtype()));
775+
769776
const symbol_exprt real_pointer_symbol = gen_nondet_subtype_pointer_init(
770777
assignments, alloc_type, replacement_pointer_type, depth);
771778

0 commit comments

Comments
 (0)