diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp index 713ffd88566..138033676b0 100644 --- a/src/java_bytecode/java_object_factory.cpp +++ b/src/java_bytecode/java_object_factory.cpp @@ -766,6 +766,13 @@ void java_object_factoryt::gen_nondet_pointer_init( // for java types, technical debt TG-2707 if(!equal_java_types(replacement_pointer_type, pointer_type)) { + // update generic_parameter_specialization_map for the new pointer + generic_parameter_specialization_map_keyst + generic_parameter_specialization_map_keys( + generic_parameter_specialization_map); + generic_parameter_specialization_map_keys.insert_pairs_for_pointer( + replacement_pointer_type, ns.follow(replacement_pointer_type.subtype())); + const symbol_exprt real_pointer_symbol = gen_nondet_subtype_pointer_init( assignments, alloc_type, replacement_pointer_type, depth); diff --git a/src/java_bytecode/java_types.h b/src/java_bytecode/java_types.h index e731915e64a..0e47a33a218 100644 --- a/src/java_bytecode/java_types.h +++ b/src/java_bytecode/java_types.h @@ -604,6 +604,19 @@ class java_generic_symbol_typet : public symbol_typet { return (generic_typest &)(add(ID_generic_types).get_sub()); } + + /// Check if this symbol has the given generic type. If yes, return its index + /// in the vector of generic types. + /// \param type The type we are looking for. + /// \return The index of the type in the vector of generic types. + optionalt generic_type_index(const reference_typet &type) const + { + const auto &type_pointer = + std::find(generic_types().begin(), generic_types().end(), type); + if(type_pointer != generic_types().end()) + return type_pointer - generic_types().begin(); + return {}; + } }; /// \param type: the type to check diff --git a/src/util/std_types.h b/src/util/std_types.h index f7e6189245f..877a8a54774 100644 --- a/src/util/std_types.h +++ b/src/util/std_types.h @@ -396,15 +396,22 @@ class class_typet:public struct_typet bases().push_back(baset(base)); } - bool has_base(const irep_idt &id) const + /// Return the base with the given name, if exists. + /// \param id The name of the base we are looking for. + /// \return The base if exists. + optionalt get_base(const irep_idt &id) const { for(const auto &b : bases()) { - if(to_symbol_type(b.type()).get(ID_identifier)==id) - return true; + if(to_symbol_type(b.type()).get_identifier() == id) + return b; } + return {}; + } - return false; + bool has_base(const irep_idt &id) const + { + return get_base(id).has_value(); } bool is_abstract() const