From: rtrimana <rtrimana@uci.edu>
Date: Wed, 3 Jul 2019 23:13:22 +0000 (-0700)
Subject: Fixing another bug: The java.lang.StringBuilder.append(char c) needs to consider... 
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=jpf-core.git;a=commitdiff_plain;h=fb55986441b8cc5486a13c83cfb43d84acea74fe

Fixing another bug: The java.lang.StringBuilder.append(char c) needs to consider creating some array when it's set to capacity 0 and append(char c) is then called---such a call has to succeed.
---

diff --git a/examples/Reflection.java b/examples/Reflection.java
index 0918964..e486890 100644
--- a/examples/Reflection.java
+++ b/examples/Reflection.java
@@ -56,8 +56,12 @@ public class Reflection {
 	   
 	  //BigInteger bi = new BigInteger("-1");
 	  //System.out.println(bi);
+	  StringBuilder sb = new StringBuilder(0);
+	  sb.append('[');
+	  sb.append(']');
+	  System.out.println(sb.toString());
 	   
-	  /* TODO: Enumerate all methods in Class.class */ 
+	  /* TODO: Enumerate all methods in Class.class
       Method[] methods = Collection.class.getMethods();
       for(Method mth : methods) {
        	  System.out.println("===========================");
@@ -69,7 +73,7 @@ public class Reflection {
 		  System.out.println();
 		  Type returnType = mth.getGenericReturnType();
 		  System.out.println(returnType + "\n");
-      }
+      }*/
 
       /*Method[] methods = Collection.class.getMethods();
       //  Method[] methods = Class.class.getMethods();
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 a2584e5..8a3e9e9 100644
--- 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);