Skip to content

Commit 2df6d81

Browse files
author
Owen Jones
committed
Set name of java array types
1 parent 32a4186 commit 2df6d81

File tree

1 file changed

+5
-0
lines changed

1 file changed

+5
-0
lines changed

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

+5
Original file line numberDiff line numberDiff line change
@@ -720,6 +720,11 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
720720
// we have the base class, java.lang.Object, length and data
721721
// of appropriate type
722722
class_type.set_tag(symbol_type_identifier);
723+
// Note that non-array types don't have "java::" at the beginning of their
724+
// tag, and their name is "java::" + their tag. Since arrays do have
725+
// "java::" at the beginning of their tag we set the name to be the same as
726+
// the tag.
727+
class_type.set(ID_name, symbol_type_identifier);
723728

724729
class_type.components().reserve(3);
725730
class_typet::componentt base_class_component(

0 commit comments

Comments
 (0)