Merge pull request #2472 from smowton/smowton/fix/nondet-stringbuilders

Java object factory: initialize AbstractStringBuilder-derived types correctly

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 {
+
+}