From bb7871b063b91f9e1157d8fb0edaab3785747633 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Thu, 9 Aug 2018 10:06:10 +0100
Subject: [PATCH 1/2] Add and use CProverString.ofCharArray

This adds a function for converting char arrays to strings and use it
for a String constructor.
---
 src/main/java/java/lang/String.java          | 25 ++++++++++++++++++--
 src/main/java/org/cprover/CProverString.java | 22 +++++++++++++++++
 2 files changed, 45 insertions(+), 2 deletions(-)

diff --git a/src/main/java/java/lang/String.java b/src/main/java/java/lang/String.java
index ed1f381..0bd0854 100644
--- a/src/main/java/java/lang/String.java
+++ b/src/main/java/java/lang/String.java
@@ -194,6 +194,27 @@ public String(char value[]) {
         // this.value = Arrays.copyOf(value, value.length);
     }
 
+    /**
+     * Intermediary function for modelling the constructor for
+     * String(char value[], int offset, int count).
+     * The code is copied from the original String(char value[], int offset, int count).
+     */
+    private static String CProverStringOfCharArray(char value[], int offset, int count) {
+        if (offset < 0) {
+            throw new StringIndexOutOfBoundsException(offset);
+        }
+        if (count < 0) {
+            throw new StringIndexOutOfBoundsException(count);
+        }
+        // Note: offset or count might be near -1>>>1.
+        if (offset > value.length - count) {
+            throw new StringIndexOutOfBoundsException(offset + count);
+        }
+        // DIFFBLUE MODEL LIBRARY Use CProverString function instead of array copy
+        return CProverString.ofCharArray(value, offset, count);
+        // this.value = Arrays.copyOfRange(value, offset, offset+count);
+    }
+
     /**
      * Allocates a new {@code String} that contains characters from a subarray
      * of the character array argument. The {@code offset} argument is the
@@ -216,11 +237,11 @@ public String(char value[]) {
      *          characters outside the bounds of the {@code value} array
      *
      * @diffblue.limitedSupport
-     * Does not throw exceptions.
      * @diffblue.untested
      */
     public String(char value[], int offset, int count) {
-        // DIFFBLUE MODEL LIBRARY This is treated internally in CBMC
+        // DIFFBLUE MODEL LIBRARY
+        this(CProverStringOfCharArray(value, offset, count));
         // if (offset < 0) {
         //     throw new StringIndexOutOfBoundsException(offset);
         // }
diff --git a/src/main/java/org/cprover/CProverString.java b/src/main/java/org/cprover/CProverString.java
index dcd9f8c..344459c 100644
--- a/src/main/java/org/cprover/CProverString.java
+++ b/src/main/java/org/cprover/CProverString.java
@@ -388,4 +388,26 @@ public static StringBuffer insert(
         return CProver.nondetWithoutNullForNotModelled();
     }
 
+    /**
+     * Converts an array of characters to a string. This uses a loop and
+     * therefore in test-generation the {@code count} will be limited by the
+     * unwind parameter.
+     * This constrains {@code value} to not be null, its length is greater or equal to
+     * {@code offset + count} and {@code offset} and {@code count} are non-negative.
+     *
+     * @param value  array of characters which is the source to copy from
+     * @param offset index in {@code value} of the first character to copy
+     * @param count  number of characters to copy
+     * @return The created String
+     */
+    public static String ofCharArray(char value[], int offset, int count) {
+        CProver.assume(value != null);
+        CProver.assume(value.length - count >= offset
+                                   && offset >= 0 && count >= 0);
+        StringBuilder builder = new StringBuilder();
+        for(int i = 0; i < count; i++) {
+            builder.append(value[offset + i]);
+        }
+        return builder.toString();
+    }
 }

From b7ca9fd6149b7ceedf1e9638e0efb1b8d5c09572 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Thu, 9 Aug 2018 10:36:48 +0100
Subject: [PATCH 2/2] Model for StringBuilder append of char array

---
 src/main/java/java/lang/StringBuilder.java | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

diff --git a/src/main/java/java/lang/StringBuilder.java b/src/main/java/java/lang/StringBuilder.java
index 77e586b..4b942c7 100644
--- a/src/main/java/java/lang/StringBuilder.java
+++ b/src/main/java/java/lang/StringBuilder.java
@@ -241,23 +241,25 @@ public StringBuilder append(CharSequence s, int start, int end) {
      */
     @Override
     public StringBuilder append(char[] str) {
-        // DIFFBLUE MODEL LIBRARY: Handled internally by CBMC
+        // DIFFBLUE MODEL LIBRARY
+        String string = CProverString.ofCharArray(str, 0, str.length);
+        return append(string);
         // super.append(str);
         // return this;
-        return CProver.nondetWithNullForNotModelled();
     }
 
     /**
      * @throws IndexOutOfBoundsException {@inheritDoc}
-     *
-     * @diffblue.noSupport
+     * @diffblue.fullSupport
+     * @diffblue.untested
      */
     @Override
     public StringBuilder append(char[] str, int offset, int len) {
+        // DIFFBLUE MODEL LIBRARY
+        String string = new String(str, offset, len);
+        return append(string);
         // super.append(str, offset, len);
         // return this;
-        CProver.notModelled();
-        return CProver.nondetWithNullForNotModelled();
     }
 
     /**