Making add_string_type more generic

The class_name is now passed as argument so that we can reuse this
function for StringBuilder and other "String-like" classes.

Author: romainbrenguier

src/java_bytecode/java_bytecode_convert_class.cpp

@@ -50,7 +50,16 @@ class java_bytecode_convert_classt:public messaget
       convert(parse_tree.parsed_class);
     else if(string_refinement_enabled &&
             parse_tree.parsed_class.name=="java.lang.String")
-      add_string_type();
+      add_string_type("java.lang.String");
+    else if(string_refinement_enabled &&
+            parse_tree.parsed_class.name=="java.lang.StringBuilder")
+      add_string_type("java.lang.StringBuilder");
+    else if(string_refinement_enabled &&
+            parse_tree.parsed_class.name=="java.lang.CharSequence")
+      add_string_type("java.lang.CharSequence");
+    else if(string_refinement_enabled &&
+            parse_tree.parsed_class.name=="java.lang.StringBuffer")
+      add_string_type("java.lang.StringBuffer");
     else
       generate_class_stub(parse_tree.parsed_class.name);
   }
@@ -72,7 +81,7 @@ class java_bytecode_convert_classt:public messaget
 
   void generate_class_stub(const irep_idt &class_name);
   void add_array_types();
-  void add_string_type();
+  void add_string_type(const irep_idt &class_name);
 };
 
 /*******************************************************************\
@@ -406,15 +415,17 @@ bool java_bytecode_convert_class(
 
 Function: java_bytecode_convert_classt::add_string_type
 
+  Inputs: a name for the class such as "java.lang.String"
+
  Purpose: Implements the java.lang.String type in the case that
           we provide an internal implementation.
 
 \*******************************************************************/
 
-void java_bytecode_convert_classt::add_string_type()
+void java_bytecode_convert_classt::add_string_type(const irep_idt &class_name)
 {
   class_typet string_type;
-  string_type.set_tag("java.lang.String");
+  string_type.set_tag(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");
@@ -432,8 +443,8 @@ void java_bytecode_convert_classt::add_string_type()
   string_type.add_base(symbol_typet("java::java.lang.Object"));
 
   symbolt string_symbol;
-  string_symbol.name="java::java.lang.String";
-  string_symbol.base_name="java.lang.String";
+  string_symbol.name="java::"+id2string(class_name);
+  string_symbol.base_name=id2string(class_name);
   string_symbol.type=string_type;
   string_symbol.is_type=true;
 
@@ -445,8 +456,8 @@ void java_bytecode_convert_classt::add_string_type()
   symbolt string_equals_symbol;
   string_equals_symbol.name=
     "java::java.lang.String.equals:(Ljava/lang/Object;)Z";
-  string_equals_symbol.base_name="java.lang.String.equals";
-  string_equals_symbol.pretty_name="java.lang.String.equals";
+  string_equals_symbol.base_name=id2string(class_name)+".equals";
+  string_equals_symbol.pretty_name=id2string(class_name)+".equals";
   string_equals_symbol.mode=ID_java;
 
   code_typet string_equals_type;