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); + } + }