From 2df6d81d4446c7414c976ef9c8a89ea9ad3c04d5 Mon Sep 17 00:00:00 2001 From: Owen Jones Date: Fri, 15 Jun 2018 13:17:27 +0100 Subject: [PATCH] Set name of java array types --- jbmc/src/java_bytecode/java_bytecode_convert_class.cpp | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp index 52f79249fad..89aec06e48f 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp @@ -720,6 +720,11 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table) // we have the base class, java.lang.Object, length and data // of appropriate type class_type.set_tag(symbol_type_identifier); + // Note that non-array types don't have "java::" at the beginning of their + // tag, and their name is "java::" + their tag. Since arrays do have + // "java::" at the beginning of their tag we set the name to be the same as + // the tag. + class_type.set(ID_name, symbol_type_identifier); class_type.components().reserve(3); class_typet::componentt base_class_component(