Added StringIndexOutOfBoundsException for charAt, with unit tests.

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