Add and use CProverString.ofCharArray

This adds a function for converting char arrays to strings and use it
for a String constructor.

Author: romainbrenguier

src/main/java/java/lang/String.java

@@ -216,21 +216,21 @@ 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
-        // 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);
-        // }
+        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
+        this(CProverString.ofCharArray(value, offset, count));
         // this.value = Arrays.copyOfRange(value, offset, offset+count);
     }
 

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 assumes {@code value} is not null, its length is greater or equal to
+     * {@code offset + count} and {@code offset} and {@code count} are positive.
+     *
+     * @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) {
+        org.cprover.CProver.assume(value != null);
+        org.cprover.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();
+    }
 }