Java object factory: initialize AbstractStringBuilder-derived types correctly

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

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

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

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

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

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

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

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

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

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

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

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

jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/test.desc

@@ -0,0 +1,12 @@
+CORE
+Test.class
+--function Test.testme
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+type mismatch
+--
+Before cbmc#2472 this would assume that StringBuilder's direct parent was
+java.lang.Object, causing a type mismatch when --refine-strings was not in use
+(which at the time would assume that parent-child relationship)

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

@@ -0,0 +1,36 @@
+public class Test {
+
+  public static void testme(StringBuilder builder, StringBuffer buffer, String str) {
+
+    // In this test the versions of String, StringBuilder and
+    // StringBuffer.class supplied have fields beyond the expected situation
+    // of either no fields at all (without --refine-strings) or only 'length'
+    // and 'data' (with --refine-strings). We check they have been nondet-
+    // initialized as expected by making sure we can reach the final
+    // 'assert false'.
+
+    if(str != null &&
+       builder != null &&
+       buffer != null &&
+       str.a != null &&
+       builder.i != null &&
+       buffer.i != null &&
+       str.a.x >= 5 &&
+       str.a.y <= -10.0f &&
+       builder.d >= 100.0 &&
+       buffer.b == true) {
+
+      assert builder instanceof StringBuilder;
+      assert buffer instanceof StringBuffer;
+      assert str instanceof String;
+
+      assert str.a instanceof A;
+      assert builder.i instanceof Integer;
+      assert buffer.i instanceof Integer;
+
+      assert false;
+    }
+
+  }
+
+}

jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/A.java

@@ -0,0 +1,8 @@
+package java.lang;
+
+public class A {
+
+  public int x;
+  public float y;
+
+}

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

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

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

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

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

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

jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/StringBuffer.java

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

jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/StringBuilder.java

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

jbmc/regression/jbmc-strings/StringModelsWithFields/test.desc

@@ -0,0 +1,14 @@
+CORE
+Test.class
+--function Test.testme
+^EXIT=10$
+^SIGNAL=0$
+assertion at file Test.java line 23 .* SUCCESS
+assertion at file Test.java line 24 .* SUCCESS
+assertion at file Test.java line 25 .* SUCCESS
+assertion at file Test.java line 27 .* SUCCESS
+assertion at file Test.java line 28 .* SUCCESS
+assertion at file Test.java line 29 .* SUCCESS
+assertion at file Test.java line 31 .* FAILURE
+--
+type mismatch