Fixed out-of-bounds cases for substring.

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 eae561c189155a02da1aef88a742a8a48e80f095..556bb7c7b594365c9c63320e9afa1172ec103874 100644 (file)
--- a/src/peers/gov/nasa/jpf/vm/JPF_java_lang_String.java
+++ b/src/peers/gov/nasa/jpf/vm/JPF_java_lang_String.java
@@ -32,7 +32,8 @@ import java.util.Locale;
  * MJI NativePeer class for java.lang.String library abstraction
  */
 public class JPF_java_lang_String extends NativePeer {
-
+  final static String sioobe = "java.lang.StringIndexOutOfBoundsException";
+  final static String sioor = "String index out of range: ";
   
   @MJI
   public int init___3CII__Ljava_lang_String_2 (MJIEnv env, int objRef, int valueRef, int offset, int count) {
@@ -145,8 +146,7 @@ public class JPF_java_lang_String extends NativePeer {
     if (index >= 0 && index < data.length) {
       return data[index];
     }
-    env.throwException("java.lang.StringIndexOutOfBoundsException",
-                      "String index out of range: " + index);
+    env.throwException(sioobe, sioor + index);
     return '\0';
   }
 
@@ -379,14 +379,24 @@ public class JPF_java_lang_String extends NativePeer {
   @MJI
   public int substring__I__Ljava_lang_String_2 (MJIEnv env, int objRef, int beginIndex) {
     String obj = env.getStringObject(objRef);
-    String result = obj.substring(beginIndex);
-    return env.newString(result);
-
+    return substring__II__Ljava_lang_String_2(env, objRef, beginIndex, obj.length());
   }
 
   @MJI
   public int substring__II__Ljava_lang_String_2 (MJIEnv env, int objRef, int beginIndex, int endIndex) {
+    if (beginIndex > endIndex) {
+      env.throwException(sioobe, sioor + (endIndex - beginIndex));
+      return 0;
+    }
+    if (beginIndex < 0) {
+      env.throwException(sioobe, sioor + beginIndex);
+      return 0;
+    }
     String obj = env.getStringObject(objRef);
+    if (endIndex > obj.length()) {
+      env.throwException(sioobe, sioor + endIndex);
+      return 0;
+    }
     String result = obj.substring(beginIndex, endIndex);
     return env.newString(result);
 

diff --git a/src/tests/gov/nasa/jpf/test/java/lang/StringTest.java b/src/tests/gov/nasa/jpf/test/java/lang/StringTest.java
index 0cd9394e8c773bb52226b2593a5907687bb5a994..7d6b709c7583dcbbc55b3cc734759836e4a10c15 100644 (file)
--- a/src/tests/gov/nasa/jpf/test/java/lang/StringTest.java
+++ b/src/tests/gov/nasa/jpf/test/java/lang/StringTest.java
@@ -187,6 +187,54 @@ public class StringTest extends TestJPF {
                }
        }
 
+       @Test
+       public void testSubstringOutOfBounds0() {
+               boolean passed = false;
+               if (verifyNoPropertyViolation()){
+                   try {
+                     " ".substring(0, 1);
+                     passed = true;
+                     " ".substring(0, 2);
+                   } catch (StringIndexOutOfBoundsException e) {
+                     assert(passed);
+                     return;
+                   }
+                   assert false;
+               }
+       }
+
+       @Test
+       public void testSubstringOutOfBounds1() {
+               boolean passed = false;
+               if (verifyNoPropertyViolation()){
+                   try {
+                     " ".substring(0, 1);
+                     passed = true;
+                     " ".substring(1, 0);
+                   } catch (StringIndexOutOfBoundsException e) {
+                     assert(passed);
+                     return;
+                   }
+                   assert false;
+               }
+       }
+
+       @Test
+       public void testSubstringOutOfBoundsNeg() {
+               boolean passed = false;
+               if (verifyNoPropertyViolation()){
+                   try {
+                     assert("".substring(0).equals(""));
+                     passed = true;
+                     " ".substring(-1);
+                   } catch (StringIndexOutOfBoundsException e) {
+                     assert(passed);
+                     return;
+                   }
+                   assert false;
+               }
+       }
+
        @Test
   @SuppressWarnings("deprecation")
   public void testConstructors(){