From: Cyrille Artho <artho@kth.se>
Date: Fri, 23 Nov 2018 13:25:43 +0000 (+0100)
Subject: Added StringIndexOutOfBoundsException for charAt, with unit tests.
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=1f2cfa01e157b4327d5ff28535710e84abdca9f3;p=jpf-core.git

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