From d08549a55ac9d8a0d06f8ca7f331e0bce44fce5f Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Fri, 23 Nov 2018 14:41:33 +0000
Subject: [PATCH 1/2] Model for String.getChars

---
 src/main/java/java/lang/String.java | 27 ++++++++++++++++-----------
 1 file changed, 16 insertions(+), 11 deletions(-)

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) {
      *            <li>{@code dstBegin+(srcEnd-srcBegin)} is larger than
      *                {@code dst.length}</ul>
      *
-     * @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);
+        }
     }
 
     /**

From f97622e01393c1a148deda08eb36c452eca88deb Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Fri, 23 Nov 2018 14:45:17 +0000
Subject: [PATCH 2/2] Model for StringBuilder.getChars

---
 src/main/java/java/lang/StringBuilder.java | 9 +++++++++
 1 file changed, 9 insertions(+)

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