Fixing another bug: The java.lang.StringBuilder.append(char c) needs to consider...

[jpf-core.git] / src / peers / gov / nasa / jpf / vm / JPF_java_lang_StringBuilder.java

diff --git a/src/peers/gov/nasa/jpf/vm/JPF_java_lang_StringBuilder.java b/src/peers/gov/nasa/jpf/vm/JPF_java_lang_StringBuilder.java
index a2584e5f674961affea047d4cd64e450889c9d66..8a3e9e937837ff414e3e113709bc8bf7c8626340 100644 (file)
--- a/src/peers/gov/nasa/jpf/vm/JPF_java_lang_StringBuilder.java
+++ b/src/peers/gov/nasa/jpf/vm/JPF_java_lang_StringBuilder.java
@@ -135,13 +135,20 @@ public class JPF_java_lang_StringBuilder extends NativePeer {
     int count = env.getIntField(objref, "count");
     int i;
     int n = count +1;
-    
+
+    // TODO: Fix for Groovy's model-checking
+    // TODO: Need to allocate something if the initial array is really empty
+    if (alen == 0) {
+      $init____V (env, objref);
+      aref = env.getReferenceField(objref, "value");
+      alen = env.getArrayLength(aref);
+    }
     if (n < alen) {
       env.setCharArrayElement(aref, count, c);
     } else {
       int m = 3 * alen / 2;
       int arefNew = env.newCharArray(m);
-      for (i=0; i<count; i++) {
+      for (i = 0; i < count; i++) {
         env.setCharArrayElement(arefNew, i, env.getCharArrayElement(aref, i));
       }
       env.setCharArrayElement(arefNew, count, c);