From: Rahmadi Trimananda <rtrimana@uci.edu>
Date: Wed, 26 Jun 2019 00:43:57 +0000 (-0700)
Subject: Fixing a bug in JPF_java_lang_String.java: There was a bug in the loop of the native... 
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=jpf-core.git;a=commitdiff_plain;h=be7d05781eb694428ccea0d45e28fec31bd52e9a

Fixing a bug in JPF_java_lang_String.java: There was a bug in the loop of the native method lastIndexOf().
---

diff --git a/examples/Reflection.java b/examples/Reflection.java
index d5041d2..ff80688 100644
--- a/examples/Reflection.java
+++ b/examples/Reflection.java
@@ -8,6 +8,8 @@ import java.util.Map;
 import java.util.ArrayList;
 import java.util.Arrays;
 
+import java.math.BigInteger;
+
 public class Reflection {
 
     interface GenericSuperShort<XYZ> {
@@ -47,10 +49,20 @@ public class Reflection {
 		  return listString;
 	   }*/
 	}
+	
+	    private static int digitsPerInt[] = {0, 0, 30, 19, 15, 13, 11,
+            11, 10, 9, 9, 8, 8, 8, 8, 7, 7, 7, 7, 7, 7, 7, 6, 6, 6, 6,
+            6, 6, 6, 6, 6, 6, 6, 6, 6, 6, 5};
+			
+		private static long bitsPerDigit[] = { 0, 0,
+            1024, 1624, 2048, 2378, 2648, 2875, 3072, 3247, 3402, 3543, 3672,
+            3790, 3899, 4001, 4096, 4186, 4271, 4350, 4426, 4498, 4567, 4633,
+            4696, 4756, 4814, 4870, 4923, 4975, 5025, 5074, 5120, 5166, 5210,
+            5253, 5295};
 
    public static void main(String[] args) {
 
-      Method[] methods = SampleClass.class.getMethods();
+      /*Method[] methods = SampleClass.class.getMethods();
       //  Method[] methods = Class.class.getMethods();
         Method method = null;
         for(Method meth : methods) {
@@ -65,8 +77,78 @@ public class Reflection {
       }
       System.out.println();
       Type returnType = method.getGenericReturnType();
-      System.out.println(returnType);
-      
+	  Class.class.getSimpleName();*/
+      //System.out.println(returnType);
+      BigInteger bi = new BigInteger("-1");
+	  System.out.println(bi);
+	  
+        /* TODO: This is an excerpt of the BigInteger library
+		int radix = 10;
+        String val = "-1";
+        int signum = 0;
+        final int[] mag;
+
+        int cursor = 0, numDigits;
+        final int len = val.length();
+
+        if (radix < Character.MIN_RADIX || radix > Character.MAX_RADIX)
+            throw new NumberFormatException("Radix out of range");
+        if (len == 0)
+            throw new NumberFormatException("Zero length BigInteger");
+
+        // Check for at most one leading sign
+        int sign = 1;
+        int index1 = val.lastIndexOf('-');
+        int index2 = val.lastIndexOf('+');
+        if (index1 >= 0) {
+            if (index1 != 0 || index2 >= 0) {
+                throw new NumberFormatException("Illegal embedded sign character");
+            }
+            sign = -1;
+            cursor = 1;
+        } else if (index2 >= 0) {
+            if (index2 != 0) {
+                throw new NumberFormatException("Illegal embedded sign character");
+            }
+            cursor = 1;
+        }
+		System.out.println(cursor);
+        if (cursor == len)
+            throw new NumberFormatException("Zero length BigInteger");
+
+        // Skip leading zeros and compute number of digits in magnitude
+        while (cursor < len &&
+                Character.digit(val.charAt(cursor), radix) == 0) {
+            cursor++;
+        }
+
+        if (cursor == len) {
+            signum = 0;
+            //mag = ZERO.mag;
+            //mag = null;
+            return;
+        }
+
+        numDigits = len - cursor;
+        signum = sign;
+
+        long numBits = ((numDigits * bitsPerDigit[radix]) >>> 10) + 1;
+        if (numBits + 31 >= (1L << 32)) {
+            System.out.println("Overflow!");
+        }
+        int numWords = (int) (numBits + 31) >>> 5;
+        int[] magnitude = new int[numWords];
+
+        // Process first (potentially short) digit group
+        int firstGroupLen = numDigits % digitsPerInt[radix];
+        if (firstGroupLen == 0)
+            firstGroupLen = digitsPerInt[radix];
+		int cursor2 = cursor + firstGroupLen;
+        String group = val.substring(cursor, cursor2);
+        magnitude[numWords - 1] = Integer.parseInt(group, radix);
+        if (magnitude[numWords - 1] < 0)
+            throw new NumberFormatException("Illegal digit");*/
+	  
       /*Type superCls = Generic.class.getGenericSuperclass();
       //Type superCls = String.class.getGenericSuperclass();
       System.out.println(superCls);
@@ -128,7 +210,6 @@ public class Reflection {
           System.out.println(bound);
       }
       System.out.println();*/
-  
    }
 }
 
diff --git a/src/peers/gov/nasa/jpf/vm/JPF_java_lang_String.java b/src/peers/gov/nasa/jpf/vm/JPF_java_lang_String.java
index 556bb7c..587a552 100644
--- a/src/peers/gov/nasa/jpf/vm/JPF_java_lang_String.java
+++ b/src/peers/gov/nasa/jpf/vm/JPF_java_lang_String.java
@@ -345,7 +345,7 @@ public class JPF_java_lang_String extends NativePeer {
       fromIndex = len - 1;
     }
 
-    for (int i = fromIndex; i > 0; i--) {
+    for (int i = fromIndex; i >= 0; i--) {
       if (values[i] == c) { return i; }
     }