Fixing another bug: The java.lang.StringBuilder.append(char c) needs to consider...
authorrtrimana <rtrimana@uci.edu>
Wed, 3 Jul 2019 23:13:22 +0000 (16:13 -0700)
committerrtrimana <rtrimana@uci.edu>
Wed, 3 Jul 2019 23:13:22 +0000 (16:13 -0700)
examples/Reflection.java
src/peers/gov/nasa/jpf/vm/JPF_java_lang_StringBuilder.java

index 0918964..e486890 100644 (file)
@@ -56,8 +56,12 @@ public class Reflection {
           
          //BigInteger bi = new BigInteger("-1");
          //System.out.println(bi);
           
          //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("===========================");
       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");
                  System.out.println();
                  Type returnType = mth.getGenericReturnType();
                  System.out.println(returnType + "\n");
-      }
+      }*/
 
       /*Method[] methods = Collection.class.getMethods();
       //  Method[] methods = Class.class.getMethods();
 
       /*Method[] methods = Collection.class.getMethods();
       //  Method[] methods = Class.class.getMethods();
index a2584e5..8a3e9e9 100644 (file)
@@ -135,13 +135,20 @@ public class JPF_java_lang_StringBuilder extends NativePeer {
     int count = env.getIntField(objref, "count");
     int i;
     int n = count +1;
     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);
     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);
         env.setCharArrayElement(arefNew, i, env.getCharArrayElement(aref, i));
       }
       env.setCharArrayElement(arefNew, count, c);