diff --git a/src/java_bytecode/generate_java_generic_type.cpp b/src/java_bytecode/generate_java_generic_type.cpp index 2b5badb381b..7edcdf08bd1 100644 --- a/src/java_bytecode/generate_java_generic_type.cpp +++ b/src/java_bytecode/generate_java_generic_type.cpp @@ -70,13 +70,20 @@ symbolt generate_java_generic_typet::operator()( pre_modification_size==after_modification_size, "All components in the original class should be in the new class"); - const auto expected_symbol="java::"+id2string(new_tag); + const java_class_typet &new_java_class = construct_specialised_generic_type( + generic_class_definition, new_tag, replacement_components); + const type_symbolt &class_symbol = + build_symbol_from_specialised_class(new_java_class); + + std::pair res = symbol_table.insert(std::move(class_symbol)); + if(!res.second) + { + messaget message(message_handler); + message.warning() << "stub class symbol " << class_symbol.name + << " already exists" << messaget::eom; + } - generate_class_stub( - new_tag, - symbol_table, - message_handler, - replacement_components); + const auto expected_symbol="java::"+id2string(new_tag); auto symbol=symbol_table.lookup(expected_symbol); INVARIANT(symbol, "New class not created"); return *symbol; @@ -216,3 +223,38 @@ irep_idt generate_java_generic_typet::build_generic_tag( return new_tag_buffer.str(); } + +/// Build the specalised version of the specific class, with the specified +/// parameters and name. +/// \param generic_class_definition: The generic class we are specialising +/// \param new_tag: The new name for the class (like Generic) +/// \param new_components: The specialised components +/// \return The newly constructed class. +java_class_typet +generate_java_generic_typet::construct_specialised_generic_type( + const java_generic_class_typet &generic_class_definition, + const irep_idt &new_tag, + const struct_typet::componentst &new_components) const +{ + java_class_typet specialised_class = generic_class_definition; + // We are specialising the logic - so we don't want to be marked as generic + specialised_class.set(ID_C_java_generics_class_type, false); + specialised_class.set(ID_name, "java::" + id2string(new_tag)); + specialised_class.set(ID_base_name, new_tag); + specialised_class.components() = new_components; + return specialised_class; +} + +/// Construct the symbol to be moved into the symbol table +/// \param specialised_class: The newly constructed specialised class +/// \return The symbol to add to the symbol table +type_symbolt generate_java_generic_typet::build_symbol_from_specialised_class( + const java_class_typet &specialised_class) const +{ + type_symbolt new_symbol(specialised_class); + new_symbol.base_name = specialised_class.get(ID_base_name); + new_symbol.pretty_name = specialised_class.get(ID_base_name); + new_symbol.name = specialised_class.get(ID_name); + new_symbol.mode = ID_java; + return new_symbol; +} diff --git a/src/java_bytecode/generate_java_generic_type.h b/src/java_bytecode/generate_java_generic_type.h index 601c32ca7a6..f7e7656abc7 100644 --- a/src/java_bytecode/generate_java_generic_type.h +++ b/src/java_bytecode/generate_java_generic_type.h @@ -33,6 +33,14 @@ class generate_java_generic_typet const java_generic_class_typet &replacement_type, const java_generic_typet &generic_reference) const; + java_class_typet construct_specialised_generic_type( + const java_generic_class_typet &generic_class_definition, + const irep_idt &new_tag, + const struct_typet::componentst &new_components) const; + + type_symbolt build_symbol_from_specialised_class( + const java_class_typet &specialised_class) const; + message_handlert &message_handler; }; diff --git a/unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp b/unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp index 1e7d52981a2..81be01d6c2b 100644 --- a/unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp +++ b/unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp @@ -153,22 +153,22 @@ SCENARIO( REQUIRE(new_symbol_table.has_symbol(first_expected_symbol)); auto first_symbol=new_symbol_table.lookup(first_expected_symbol); REQUIRE(first_symbol->type.id()==ID_struct); - auto first_symbol_type= - to_struct_type(first_symbol->type).components()[3].type(); - REQUIRE(first_symbol_type.id()==ID_pointer); - REQUIRE(first_symbol_type.subtype().id()==ID_symbol); - REQUIRE(to_symbol_type(first_symbol_type.subtype()).get_identifier()== - "java::java.lang.Boolean"); + const struct_union_typet::componentt &component = + require_type::require_component( + to_struct_type(first_symbol->type), "elem"); + auto first_symbol_type=component.type(); + require_type::require_pointer( + first_symbol_type, symbol_typet("java::java.lang.Boolean")); REQUIRE(new_symbol_table.has_symbol(second_expected_symbol)); auto second_symbol=new_symbol_table.lookup(second_expected_symbol); REQUIRE(second_symbol->type.id()==ID_struct); - auto second_symbol_type= - to_struct_type(second_symbol->type).components()[3].type(); - REQUIRE(second_symbol_type.id()==ID_pointer); - REQUIRE(second_symbol_type.subtype().id()==ID_symbol); - REQUIRE(to_symbol_type(second_symbol_type.subtype()).get_identifier()== - "java::java.lang.Integer"); + const struct_union_typet::componentt &second_component = + require_type::require_component( + to_struct_type(second_symbol->type), "elem"); + auto second_symbol_type=second_component.type(); + require_type::require_pointer( + second_symbol_type, symbol_typet("java::java.lang.Integer")); } }