Fixed out-of-bounds cases for substring.

[jpf-core.git] / src / tests / gov / nasa / jpf / test / java / lang / StringTest.java

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(){