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 7ea813cc4d9..b4c1a7ea07a 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 @@ -13,7 +13,8 @@ #include #include - +#include +#include SCENARIO( "generate_java_generic_type_from_file", @@ -160,3 +161,64 @@ SCENARIO( "java::java.lang.Integer"); } } + +SCENARIO( + "generate_java_generic_type_with_array_concrete_type", + "[core][java_bytecode][generate_java_generic_type]") +{ + // We have a 'harness' class who's only purpose is to contain a reference + // to the generic class so that we can test the specialization of that generic + // class + const irep_idt harness_class= + "java::generic_field_array_instantiation"; + + // We want to test that the specialized/instantiated class has it's field + // type updated, so find the specialized class, not the generic class. + const irep_idt test_class= + "java::generic_field_array_instantiation$generic"; + + GIVEN("A generic type instantiated with an array type") + { + symbol_tablet new_symbol_table= + load_java_class( + "generic_field_array_instantiation", + "./java_bytecode/generate_concrete_generic_type"); + + // Ensure the class has been specialized + REQUIRE(new_symbol_table.has_symbol(harness_class)); + const symbolt &harness_symbol= + new_symbol_table.lookup_ref(harness_class); + + const struct_typet::componentt &harness_component= + require_type::require_component( + to_struct_type(harness_symbol.type), + "f"); + + ui_message_handlert message_handler; + generate_java_generic_typet instantiate_generic_type(message_handler); + instantiate_generic_type( + to_java_generic_type(harness_component.type()), new_symbol_table); + + // Test the specialized class + REQUIRE(new_symbol_table.has_symbol(test_class)); + const symbolt test_class_symbol= + new_symbol_table.lookup_ref(test_class); + + REQUIRE(test_class_symbol.type.id()==ID_struct); + const struct_typet::componentt &field_component= + require_type::require_component( + to_struct_type(test_class_symbol.type), + "gf"); + const typet &test_field_type=field_component.type(); + + REQUIRE(test_field_type.id()==ID_pointer); + REQUIRE(test_field_type.subtype().id()==ID_symbol); + const symbol_typet test_field_array= + to_symbol_type(test_field_type.subtype()); + REQUIRE(test_field_array.get_identifier()=="java::array[reference]"); + const pointer_typet &element_type= + require_type::require_pointer( + java_array_element_type(test_field_array), + symbol_typet("java::java.lang.Float")); + } +} diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation$generic.class b/unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation$generic.class new file mode 100644 index 00000000000..b7056a5e522 Binary files /dev/null and b/unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation$generic.class differ diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation.class b/unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation.class new file mode 100644 index 00000000000..67141fda96a Binary files /dev/null and b/unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation.class differ diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation.java b/unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation.java new file mode 100644 index 00000000000..c5266feeedb --- /dev/null +++ b/unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation.java @@ -0,0 +1,11 @@ +public class generic_field_array_instantiation { + + class generic { + T gf; + } + + generic f; + Float [] af; +} + +