Merge pull request diffblue#2479 from thk123/bugfix/TG-3908/give-string-objects-names

Given string types an appropriate name [TG-3908]

Author: Thomas Kiley

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -393,7 +393,7 @@ void java_bytecode_convert_classt::convert(
   new_symbol.base_name = base_name;
   new_symbol.pretty_name=c.name;
   new_symbol.name=qualified_classname;
-  class_type.set(ID_name, new_symbol.name);
+  class_type.set_name(new_symbol.name);
   new_symbol.type=class_type;
   new_symbol.mode=ID_java;
   new_symbol.is_type=true;
@@ -716,15 +716,15 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
     if(symbol_table.has_symbol(symbol_type_identifier))
       return;
 
-    class_typet class_type;
+    java_class_typet class_type;
     // 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.set_name(symbol_type_identifier);
 
     class_type.components().reserve(3);
     class_typet::componentt base_class_component(

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

@@ -222,6 +222,7 @@ void java_string_library_preprocesst::add_string_type(
 {
   java_class_typet string_type;
   string_type.set_tag(class_name);
+  string_type.set_name("java::" + id2string(class_name));
   string_type.components().resize(3);
   string_type.components()[0].set_name("@java.lang.Object");
   string_type.components()[0].set_pretty_name("@java.lang.Object");

jbmc/src/java_bytecode/java_types.h

@@ -158,6 +158,20 @@ class java_class_typet:public class_typet
     return type_checked_cast<annotated_typet>(
       static_cast<typet &>(*this)).get_annotations();
   }
+
+  /// Get the name of the struct, which can be used to look up its symbol
+  /// in the symbol table.
+  const irep_idt &get_name() const
+  {
+    return get(ID_name);
+  }
+
+  /// Set the name of the struct, which can be used to look up its symbol
+  /// in the symbol table.
+  void set_name(const irep_idt &name)
+  {
+    set(ID_name, name);
+  }
 };
 
 inline const java_class_typet &to_java_class_type(const typet &type)

jbmc/src/java_bytecode/java_utils.cpp

@@ -67,7 +67,7 @@ void generate_class_stub(
   message_handlert &message_handler,
   const struct_union_typet::componentst &componentst)
 {
-  class_typet class_type;
+  java_class_typet class_type;
 
   class_type.set_tag(class_name);
   class_type.set(ID_base_name, class_name);
@@ -79,7 +79,7 @@ void generate_class_stub(
   new_symbol.base_name=class_name;
   new_symbol.pretty_name=class_name;
   new_symbol.name="java::"+id2string(class_name);
-  class_type.set(ID_name, new_symbol.name);
+  class_type.set_name(new_symbol.name);
   new_symbol.type=class_type;
   new_symbol.mode=ID_java;
   new_symbol.is_type=true;