X-Git-Url: http://plrg.eecs.uci.edu/git/?p=jpf-core.git;a=blobdiff_plain;f=src%2Ftests%2Fgov%2Fnasa%2Fjpf%2Ftest%2Fjava%2Flang%2FStringTest.java;h=7d6b709c7583dcbbc55b3cc734759836e4a10c15;hp=0cd9394e8c773bb52226b2593a5907687bb5a994;hb=b592174fd5484cb641f1039a4eccc8af6e8c525f;hpb=1f2cfa01e157b4327d5ff28535710e84abdca9f3

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 0cd9394..7d6b709 100644
--- 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(){