diff --git a/src/main/java/java/lang/String.java b/src/main/java/java/lang/String.java
index 8f4527e..ae87214 100644
--- a/src/main/java/java/lang/String.java
+++ b/src/main/java/java/lang/String.java
@@ -964,20 +964,25 @@ public int offsetByCodePoints(int index, int codePointOffset) {
*
{@code dstBegin+(srcEnd-srcBegin)} is larger than
* {@code dst.length}
*
- * @diffblue.noSupport
+ * @diffblue.fullSupport
+ * @diffblue.untested
*/
public void getChars(int srcBegin, int srcEnd, char dst[], int dstBegin) {
- CProver.notModelled();
- // if (srcBegin < 0) {
- // throw new StringIndexOutOfBoundsException(srcBegin);
- // }
- // if (srcEnd > value.length) {
- // throw new StringIndexOutOfBoundsException(srcEnd);
- // }
- // if (srcBegin > srcEnd) {
- // throw new StringIndexOutOfBoundsException(srcEnd - srcBegin);
- // }
+ if (srcBegin < 0) {
+ throw new StringIndexOutOfBoundsException(srcBegin);
+ }
+ if (srcEnd > length()) {
+ throw new StringIndexOutOfBoundsException(srcEnd);
+ }
+ if (srcBegin > srcEnd) {
+ throw new StringIndexOutOfBoundsException(srcEnd - srcBegin);
+ }
+ // DIFFBLUE MODEL LIBRARY we inline System.arraycopy here so that we
+ // can specialize it for characters.
// System.arraycopy(value, srcBegin, dst, dstBegin, srcEnd - srcBegin);
+ for(int i = 0; i < srcEnd - srcBegin; i++) {
+ dst[dstBegin + i] = CProverString.charAt(this, srcBegin + i);
+ }
}
/**
diff --git a/src/main/java/java/lang/StringBuilder.java b/src/main/java/java/lang/StringBuilder.java
index 4b942c7..d583dad 100644
--- a/src/main/java/java/lang/StringBuilder.java
+++ b/src/main/java/java/lang/StringBuilder.java
@@ -662,4 +662,13 @@ public String toString() {
// value = (char[]) s.readObject();
// }
+ // DIFFBLUE MODEL LIBRARY This should be inherited from AbstractStringBuilder
+ /**
+ * @diffblue.fullSupport
+ * @diffblue.untested
+ */
+ public void getChars(int srcBegin, int srcEnd, char dst[], int dstBegin) {
+ toString().getChars(srcBegin, srcEnd, dst, dstBegin);
+ }
+
}