Added StringIndexOutOfBoundsException for charAt, with unit tests.

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 34a257938a2222d36974d52e2e9c3fa59bb71797..eae561c189155a02da1aef88a742a8a48e80f095 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
@@ -142,7 +142,12 @@ public class JPF_java_lang_String extends NativePeer {
   @MJI
   public char charAt__I__C (MJIEnv env, int objRef, int index){
     char[] data = env.getStringChars(objRef);
-    return data[index];
+    if (index >= 0 && index < data.length) {
+      return data[index];
+    }
+    env.throwException("java.lang.StringIndexOutOfBoundsException",
+                      "String index out of range: " + index);
+    return '\0';
   }
 
   

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 efbe6d7f545713ac9512939f19c7daaf2eb835e6..0cd9394e8c773bb52226b2593a5907687bb5a994 100644 (file)
--- a/src/tests/gov/nasa/jpf/test/java/lang/StringTest.java
+++ b/src/tests/gov/nasa/jpf/test/java/lang/StringTest.java
@@ -159,6 +159,34 @@ public class StringTest extends TestJPF {
                }
        }
 
+       @Test
+       public void testCharAtOutOfBounds() {
+               if (verifyNoPropertyViolation()){
+                   try {
+                     "".charAt(0);
+                   } catch (StringIndexOutOfBoundsException e) {
+                     return;
+                   }
+                   assert false;
+               }
+       }
+
+       @Test
+       public void testCharAtOutOfBoundsNeg() {
+               boolean passed = false;
+               if (verifyNoPropertyViolation()){
+                   try {
+                     assert(" ".charAt(0) == ' ');
+                     passed = true;
+                     " ".charAt(-1);
+                   } catch (StringIndexOutOfBoundsException e) {
+                     assert(passed);
+                     return;
+                   }
+                   assert false;
+               }
+       }
+
        @Test
   @SuppressWarnings("deprecation")
   public void testConstructors(){