Added StringIndexOutOfBoundsException for charAt, with unit tests.
authorCyrille Artho <artho@kth.se>
Fri, 23 Nov 2018 13:25:43 +0000 (14:25 +0100)
committerCyrille Artho <artho@kth.se>
Fri, 23 Nov 2018 13:25:43 +0000 (14:25 +0100)
src/peers/gov/nasa/jpf/vm/JPF_java_lang_String.java
src/tests/gov/nasa/jpf/test/java/lang/StringTest.java

index 34a2579..eae561c 100644 (file)
@@ -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';
   }
 
   
index efbe6d7..0cd9394 100644 (file)
@@ -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(){