@@ -184,8 +184,9 @@ SCENARIO(
184184
185185 // We want to test that the specialized/instantiated class has it's field
186186 // type updated, so find the specialized class, not the generic class.
187- const irep_idt test_class=
188- " java::generic_field_array_instantiation$generic<java::array[reference]>" ;
187+ const irep_idt test_class =
188+ " java::generic_field_array_instantiation$generic<java::array[reference]"
189+ " of_java::java.lang.Float>" ;
189190
190191 GIVEN (" A generic type instantiated with an array type" )
191192 {
@@ -230,5 +231,42 @@ SCENARIO(
230231 require_type::require_pointer (
231232 java_array_element_type (test_field_array),
232233 symbol_typet (" java::java.lang.Float" ));
234+
235+ // check for other specialized classes, in particular different symbol ids
236+ // for arrays with different element types
237+ GIVEN (" A generic type instantiated with different array types" )
238+ {
239+ const irep_idt test_class_integer =
240+ " java::generic_field_array_instantiation$generic<java::array[reference]"
241+ " of_"
242+ " java::java.lang.Integer>" ;
243+
244+ const irep_idt test_class_int =
245+ " java::generic_field_array_instantiation$generic<java::array[int]>" ;
246+
247+ const irep_idt test_class_float =
248+ " java::generic_field_array_instantiation$generic<java::array[float]>" ;
249+
250+ const struct_typet::componentt &component_g =
251+ require_type::require_component (
252+ to_struct_type (harness_symbol.type ), " g" );
253+ instantiate_generic_type (
254+ to_java_generic_type (component_g.type ()), new_symbol_table);
255+ REQUIRE (new_symbol_table.has_symbol (test_class_integer));
256+
257+ const struct_typet::componentt &component_h =
258+ require_type::require_component (
259+ to_struct_type (harness_symbol.type ), " h" );
260+ instantiate_generic_type (
261+ to_java_generic_type (component_h.type ()), new_symbol_table);
262+ REQUIRE (new_symbol_table.has_symbol (test_class_int));
263+
264+ const struct_typet::componentt &component_i =
265+ require_type::require_component (
266+ to_struct_type (harness_symbol.type ), " i" );
267+ instantiate_generic_type (
268+ to_java_generic_type (component_i.type ()), new_symbol_table);
269+ REQUIRE (new_symbol_table.has_symbol (test_class_float));
270+ }
233271 }
234272}
0 commit comments