Java object factory: initialize AbstractStringBuilder-derived types correctly

These are currently initialized as if they are directly derived from Object, which causes a crash due to the
type inconsistency between StringBuilder { AbstractStringBuilder { Object { } } } and StringBuilder { Object { } }

Author: smowton

jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/Test.class

@@ -0,0 +1,7 @@
+public class Test {
+
+  public static void testme(StringBuilder builder, StringBuffer buffer) {
+
+  }
+
+}

jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/Test.java

@@ -0,0 +1,5 @@
+package java.lang;
+
+public class AbstractStringBuilder implements CharSequence {
+
+}

jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/AbstractStringBuilder.class

@@ -0,0 +1,5 @@
+package java.lang;
+
+interface CharSequence {
+
+}

jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/AbstractStringBuilder.java

@@ -0,0 +1,5 @@
+package java.lang;
+
+public class String implements CharSequence {
+
+}

jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/CharSequence.class

@@ -0,0 +1,5 @@
+package java.lang;
+
+public class StringBuffer extends AbstractStringBuilder {
+
+}

jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/CharSequence.java

@@ -0,0 +1,5 @@
+package java.lang;
+
+public class StringBuilder extends AbstractStringBuilder {
+
+}

jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/String.class

@@ -0,0 +1,7 @@
+CORE
+Test.class
+--function Test.testme
+^EXIT=0$
+^SIGNAL=0$
+--
+type mismatch

jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/String.java

@@ -570,13 +570,18 @@ codet initialize_nondet_string_struct(
     ? "java::java.lang.String"
     : "java::" + id2string(struct_type.get_tag());
 
-  const symbol_typet jlo_symbol("java::java.lang.Object");
-  const struct_typet &jlo_type = to_struct_type(ns.follow(jlo_symbol));
-  struct_exprt jlo_init(jlo_symbol);
-  java_root_class_init(jlo_init, jlo_type, class_id);
+  const struct_typet &superclass_type =
+    to_struct_type(ns.follow(struct_type.components().at(0).type()));
+
+  null_message_handlert nullout;
+  exprt superclass_init =
+    zero_initializer(superclass_type, loc, ns, nullout);
+
+  set_class_identifier(
+    to_struct_expr(superclass_init), ns, symbol_typet(class_id));
 
   struct_exprt struct_expr(obj.type());
-  struct_expr.copy_to_operands(jlo_init);
+  struct_expr.copy_to_operands(superclass_init);
 
   // In case the type for string was not added to the symbol table,
   // (typically when string refinement is not activated), `struct_type`