Skip to content

Commit

Permalink
Set name of java array types
Browse files Browse the repository at this point in the history
  • Loading branch information
Owen Jones committed Jun 18, 2018
1 parent 32a4186 commit 2df6d81
Showing 1 changed file with 5 additions and 0 deletions.
5 changes: 5 additions & 0 deletions jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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(
Expand Down

0 comments on commit 2df6d81

Please sign in to comment.