/*

* Copyright (c) 1994, 2013, Oracle and/or its affiliates. All rights reserved.

* DO NOT ALTER OR REMOVE COPYRIGHT NOTICES OR THIS FILE HEADER.

*

* This code is free software; you can redistribute it and/or modify it

* under the terms of the GNU General Public License version 2 only, as

* published by the Free Software Foundation. Oracle designates this

* particular file as subject to the "Classpath" exception as provided

* by Oracle in the LICENSE file that accompanied this code.

*

* This code is distributed in the hope that it will be useful, but WITHOUT

* ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or

* FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License

* version 2 for more details (a copy is included in the LICENSE file that

* accompanied this code).

*

* You should have received a copy of the GNU General Public License version

* 2 along with this work; if not, write to the Free Software Foundation,

* Inc., 51 Franklin St, Fifth Floor, Boston, MA 02110-1301 USA.

*

* Please contact Oracle, 500 Oracle Parkway, Redwood Shores, CA 94065 USA

* or visit www.oracle.com if you need additional information or have any

* questions.

*/

package java.lang;

import java.io.UnsupportedEncodingException;

import java.nio.charset.Charset;

import java.util.Comparator;

import java.util.Iterator;

import java.util.Locale;

// DIFFBLUE MODEL LIBRARY these headers are not used

// import java.io.ObjectStreamField;

// import java.util.ArrayList;

// import java.util.Arrays;

// import java.util.Formatter;

// import java.util.Objects;

// import java.util.StringJoiner;

// import java.util.regex.Matcher;

// import java.util.regex.Pattern;

// import java.util.regex.PatternSyntaxException;

// DIFFBLUE MODEL LIBRARY new imports in the model

import java.nio.charset.StandardCharsets;

import org.cprover.CProver;

// Used as an interface with CProver internal string functions:

import org.cprover.CProverString;

/**

* The {@code String} class represents character strings. All

* string literals in Java programs, such as {@code "abc"}, are

* implemented as instances of this class.

* <p>

* Strings are constant; their values cannot be changed after they

* are created. String buffers support mutable strings.

* Because String objects are immutable they can be shared. For example:

* <blockquote><pre>

* String str = "abc";

* </pre></blockquote><p>

* is equivalent to:

* <blockquote><pre>

* char data[] = {'a', 'b', 'c'};

* String str = new String(data);

* </pre></blockquote><p>

* Here are some more examples of how strings can be used:

* <blockquote><pre>

* System.out.println("abc");

* String cde = "cde";

* System.out.println("abc" + cde);

* String c = "abc".substring(2,3);

* String d = cde.substring(1, 2);

* </pre></blockquote>

* <p>

* The class {@code String} includes methods for examining

* individual characters of the sequence, for comparing strings, for

* searching strings, for extracting substrings, and for creating a

* copy of a string with all characters translated to uppercase or to

* lowercase. Case mapping is based on the Unicode Standard version

* specified by the {@link java.lang.Character Character} class.

* <p>

* The Java language provides special support for the string

* concatenation operator (&nbsp;+&nbsp;), and for conversion of

* other objects to strings. String concatenation is implemented

* through the {@code StringBuilder}(or {@code StringBuffer})

* class and its {@code append} method.

* String conversions are implemented through the method

* {@code toString}, defined by {@code Object} and

* inherited by all classes in Java. For additional information on

* string concatenation and conversion, see Gosling, Joy, and Steele,

* <i>The Java Language Specification</i>.

*

* <p> Unless otherwise noted, passing a <tt>null</tt> argument to a constructor

* or method in this class will cause a {@link NullPointerException} to be

* thrown.

*

* <p>A {@code String} represents a string in the UTF-16 format

* in which <em>supplementary characters</em> are represented by <em>surrogate

* pairs</em> (see the section <a href="Character.html#unicode">Unicode

* Character Representations</a> in the {@code Character} class for

* more information).

* Index values refer to {@code char} code units, so a supplementary

* character uses two positions in a {@code String}.

* <p>The {@code String} class provides methods for dealing with

* Unicode code points (i.e., characters), in addition to those for

* dealing with Unicode code units (i.e., {@code char} values).

*

* @author Lee Boynton

* @author Arthur van Hoff

* @author Martin Buchholz

* @author Ulf Zibis

* @see java.lang.Object#toString()

* @see java.lang.StringBuffer

* @see java.lang.StringBuilder

* @see java.nio.charset.Charset

* @since JDK1.0

*

* @diffblue.limitedSupport

* Not all methods are fully supported.

*/

public final class String

implements java.io.Serializable, Comparable<String>, CharSequence {

/** The value is used for character storage. */

// DIFFBLUE MODEL LIBRARY This is treated internally in CBMC

// private final char value[];

/** Cache the hash code for the string */

// DIFFBLUE MODEL LIBRARY This is not necessary for modelling

// private int hash; // Default to 0

/** use serialVersionUID from JDK 1.0.2 for interoperability */

private static final long serialVersionUID = -6849794470754667710L;

/**

* Class String is special cased within the Serialization Stream Protocol.

*

* A String instance is written into an ObjectOutputStream according to

* <a href="{@docRoot}/../platform/serialization/spec/output.html">

* Object Serialization Specification, Section 6.2, "Stream Elements"</a>

*/

// DIFFBLUE MODEL LIBRARY This is not necessary for modelling

// private static final ObjectStreamField[] serialPersistentFields =

// new ObjectStreamField[0];

/**

* Initializes a newly created {@code String} object so that it represents

* an empty character sequence. Note that use of this constructor is

* unnecessary since Strings are immutable.

*

* @diffblue.fullSupport

* @diffblue.untested

*/

public String() {

// DIFFBLUE MODEL LIBRARY This is treated internally in CBMC

// this.value = new char[0];

}

/**

* Initializes a newly created {@code String} object so that it represents

* the same sequence of characters as the argument; in other words, the

* newly created string is a copy of the argument string. Unless an

* explicit copy of {@code original} is needed, use of this constructor is

* unnecessary since Strings are immutable.

*

* @param original

* A {@code String}

*

* @diffblue.fullSupport

* @diffblue.untested

*/

public String(String original) {

// DIFFBLUE MODEL LIBRARY This is treated internally in CBMC

// this.value = original.value;

// this.hash = original.hash;

}

/**

* Allocates a new {@code String} so that it represents the sequence of

* characters currently contained in the character array argument. The

* contents of the character array are copied; subsequent modification of

* the character array does not affect the newly created string.

*

* @param value

* The initial value of the string

*

* @diffblue.noSupport

* @diffblue.todo implement using the version with offset and count arguments

*/

public String(char value[]) {

CProver.notModelled();

// this.value = Arrays.copyOf(value, value.length);

}

/**

* Allocates a new {@code String} that contains characters from a subarray

* of the character array argument. The {@code offset} argument is the

* index of the first character of the subarray and the {@code count}

* argument specifies the length of the subarray. The contents of the

* subarray are copied; subsequent modification of the character array does

* not affect the newly created string.

*

* @param value

* Array that is the source of characters

*

* @param offset

* The initial offset

*

* @param count

* The length

*

* @throws IndexOutOfBoundsException

* If the {@code offset} and {@code count} arguments index

* 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);

// }

// this.value = Arrays.copyOfRange(value, offset, offset+count);

}

/**

* Allocates a new {@code String} that contains characters from a subarray

* of the <a href="Character.html#unicode">Unicode code point</a> array

* argument. The {@code offset} argument is the index of the first code

* point of the subarray and the {@code count} argument specifies the

* length of the subarray. The contents of the subarray are converted to

* {@code char}s; subsequent modification of the {@code int} array does not

* affect the newly created string.

*

* @param codePoints

* Array that is the source of Unicode code points

*

* @param offset

* The initial offset

*

* @param count

* The length

*

* @throws IllegalArgumentException

* If any invalid Unicode code point is found in {@code

* codePoints}

*

* @throws IndexOutOfBoundsException

* If the {@code offset} and {@code count} arguments index

* characters outside the bounds of the {@code codePoints} array

*

* @since 1.5

*

* @diffblue.noSupport

* @diffblue.todo Implement assuming ASCII.

*/

public String(int[] codePoints, int offset, int count) {

CProver.notModelled();

// 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 > codePoints.length - count) {

// throw new StringIndexOutOfBoundsException(offset + count);

// }

//

// final int end = offset + count;

//

// // Pass 1: Compute precise size of char[]

// int n = count;

// for (int i = offset; i < end; i++) {

// int c = codePoints[i];

// if (Character.isBmpCodePoint(c))

// continue;

// else if (Character.isValidCodePoint(c))

// n++;

// else throw new IllegalArgumentException(Integer.toString(c));

// }

//

// // Pass 2: Allocate and fill in char[]

// final char[] v = new char[n];

//

// for (int i = offset, j = 0; i < end; i++, j++) {

// int c = codePoints[i];

// if (Character.isBmpCodePoint(c))

// v[j] = (char)c;

// else

// Character.toSurrogates(c, v, j++);

// }

//

// this.value = v;

}

/**

* Allocates a new {@code String} constructed from a subarray of an array

* of 8-bit integer values.

*

* <p> The {@code offset} argument is the index of the first byte of the

* subarray, and the {@code count} argument specifies the length of the

* subarray.

*

* <p> Each {@code byte} in the subarray is converted to a {@code char} as

* specified in the method above.

*

* @deprecated This method does not properly convert bytes into characters.

* As of JDK&nbsp;1.1, the preferred way to do this is via the

* {@code String} constructors that take a {@link

* java.nio.charset.Charset}, charset name, or that use the platform's

* default charset.

*

* @param ascii

* The bytes to be converted to characters

*

* @param hibyte

* The top 8 bits of each 16-bit Unicode code unit

*

* @param offset

* The initial offset

* @param count

* The length

*

* @throws IndexOutOfBoundsException

* If the {@code offset} or {@code count} argument is invalid

*

* @see #String(byte[], int)

* @see #String(byte[], int, int, java.lang.String)

* @see #String(byte[], int, int, java.nio.charset.Charset)

* @see #String(byte[], int, int)

* @see #String(byte[], java.lang.String)

* @see #String(byte[], java.nio.charset.Charset)

* @see #String(byte[])

*

* @diffblue.noSupport

*/

@Deprecated

public String(byte ascii[], int hibyte, int offset, int count) {

CProver.notModelled();

// checkBounds(ascii, offset, count);

// char value[] = new char[count];

//

// if (hibyte == 0) {

// for (int i = count; i-- > 0;) {

// value[i] = (char)(ascii[i + offset] & 0xff);

// }

// } else {

// hibyte <<= 8;

// for (int i = count; i-- > 0;) {

// value[i] = (char)(hibyte | (ascii[i + offset] & 0xff));

// }

// }

// this.value = value;

}

/**

* Allocates a new {@code String} containing characters constructed from

* an array of 8-bit integer values. Each character <i>c</i>in the

* resulting string is constructed from the corresponding component

* <i>b</i> in the byte array such that:

*

* <blockquote><pre>

* <b><i>c</i></b> == (char)(((hibyte &amp; 0xff) &lt;&lt; 8)

* | (<b><i>b</i></b> &amp; 0xff))

* </pre></blockquote>

*

* @deprecated This method does not properly convert bytes into

* characters. As of JDK&nbsp;1.1, the preferred way to do this is via the

* {@code String} constructors that take a {@link

* java.nio.charset.Charset}, charset name, or that use the platform's

* default charset.

*

* @param ascii

* The bytes to be converted to characters

*

* @param hibyte

* The top 8 bits of each 16-bit Unicode code unit

*

* @see #String(byte[], int, int, java.lang.String)

* @see #String(byte[], int, int, java.nio.charset.Charset)

* @see #String(byte[], int, int)

* @see #String(byte[], java.lang.String)

* @see #String(byte[], java.nio.charset.Charset)

* @see #String(byte[])

*

* @diffblue.noSupport

*/

@Deprecated

public String(byte ascii[], int hibyte) {

CProver.notModelled();

// this(ascii, hibyte, 0, ascii.length);

}

/* Common private utility method used to bounds check the byte array

* and requested offset & length values used by the String(byte[],..)

* constructors.

*/

// DIFFBLUE MODEL LIBRARY Unused private method

// private static void checkBounds(byte[] bytes, int offset, int length) {

// if (length < 0)

// throw new StringIndexOutOfBoundsException(length);

// if (offset < 0)

// throw new StringIndexOutOfBoundsException(offset);

// if (offset > bytes.length - length)

// throw new StringIndexOutOfBoundsException(offset + length);

// }

/**

* Constructs a new {@code String} by decoding the specified subarray of

* bytes using the specified charset. The length of the new {@code String}

* is a function of the charset, and hence may not be equal to the length

* of the subarray.

*

* <p> The behavior of this constructor when the given bytes are not valid

* in the given charset is unspecified. The {@link

* java.nio.charset.CharsetDecoder} class should be used when more control

* over the decoding process is required.

*

* @param bytes

* The bytes to be decoded into characters

*

* @param offset

* The index of the first byte to decode

*

* @param length

* The number of bytes to decode

* @param charsetName

* The name of a supported {@linkplain java.nio.charset.Charset

* charset}

*

* @throws UnsupportedEncodingException

* If the named charset is not supported

*

* @throws IndexOutOfBoundsException

* If the {@code offset} and {@code length} arguments index

* characters outside the bounds of the {@code bytes} array

*

* @since JDK1.1

*

* @diffblue.noSupport

* @diffblue.todo Implement assuming ASCII.

*/

public String(byte bytes[], int offset, int length, String charsetName)

throws UnsupportedEncodingException {

CProver.notModelled();

// if (charsetName == null)

// throw new NullPointerException("charsetName");

// checkBounds(bytes, offset, length);

// this.value = StringCoding.decode(charsetName, bytes, offset, length);

}

/**

* Constructs a new {@code String} by decoding the specified subarray of

* bytes using the specified {@linkplain java.nio.charset.Charset charset}.

* The length of the new {@code String} is a function of the charset, and

* hence may not be equal to the length of the subarray.

*

* <p> This method always replaces malformed-input and unmappable-character

* sequences with this charset's default replacement string. The {@link

* java.nio.charset.CharsetDecoder} class should be used when more control

* over the decoding process is required.

*

* @param bytes

* The bytes to be decoded into characters

*

* @param offset

* The index of the first byte to decode

*

* @param length

* The number of bytes to decode

*

* @param charset

* The {@linkplain java.nio.charset.Charset charset} to be used to

* decode the {@code bytes}

*

* @throws IndexOutOfBoundsException

* If the {@code offset} and {@code length} arguments index

* characters outside the bounds of the {@code bytes} array

*

* @since 1.6

*

* @diffblue.noSupport

*/

public String(byte bytes[], int offset, int length, Charset charset) {

CProver.notModelled();

// if (charset == null)

// throw new NullPointerException("charset");

// checkBounds(bytes, offset, length);

// this.value = StringCoding.decode(charset, bytes, offset, length);

}

/**

* Constructs a new {@code String} by decoding the specified array of bytes

* using the specified {@linkplain java.nio.charset.Charset charset}. The

* length of the new {@code String} is a function of the charset, and hence

* may not be equal to the length of the byte array.

*

* <p> The behavior of this constructor when the given bytes are not valid

* in the given charset is unspecified. The {@link

* java.nio.charset.CharsetDecoder} class should be used when more control

* over the decoding process is required.

*

* @param bytes

* The bytes to be decoded into characters

*

* @param charsetName

* The name of a supported {@linkplain java.nio.charset.Charset

* charset}

*

* @throws UnsupportedEncodingException

* If the named charset is not supported

*

* @since JDK1.1

*

* @diffblue.noSupport

*/

public String(byte bytes[], String charsetName)

throws UnsupportedEncodingException {

CProver.notModelled();

// this(bytes, 0, bytes.length, charsetName);

}

/**

* Constructs a new {@code String} by decoding the specified array of

* bytes using the specified {@linkplain java.nio.charset.Charset charset}.

* The length of the new {@code String} is a function of the charset, and

* hence may not be equal to the length of the byte array.

*

* <p> This method always replaces malformed-input and unmappable-character

* sequences with this charset's default replacement string. The {@link

* java.nio.charset.CharsetDecoder} class should be used when more control

* over the decoding process is required.

*

* @param bytes

* The bytes to be decoded into characters

*

* @param charset

* The {@linkplain java.nio.charset.Charset charset} to be used to

* decode the {@code bytes}

*

* @since 1.6

*

* @diffblue.noSupport

*/

public String(byte bytes[], Charset charset) {

CProver.notModelled();

// this(bytes, 0, bytes.length, charset);

}

/**

* Constructs a new {@code String} by decoding the specified subarray of

* bytes using the platform's default charset. The length of the new

* {@code String} is a function of the charset, and hence may not be equal

* to the length of the subarray.

*

* <p> The behavior of this constructor when the given bytes are not valid

* in the default charset is unspecified. The {@link

* java.nio.charset.CharsetDecoder} class should be used when more control

* over the decoding process is required.

*

* @param bytes

* The bytes to be decoded into characters

*

* @param offset

* The index of the first byte to decode

*

* @param length

* The number of bytes to decode

*

* @throws IndexOutOfBoundsException

* If the {@code offset} and the {@code length} arguments index

* characters outside the bounds of the {@code bytes} array

*

* @since JDK1.1

*

* @diffblue.noSupport

*/

public String(byte bytes[], int offset, int length) {

CProver.notModelled();

// checkBounds(bytes, offset, length);

// this.value = StringCoding.decode(bytes, offset, length);

}

/**

* Constructs a new {@code String} by decoding the specified array of bytes

* using the platform's default charset. The length of the new {@code

* String} is a function of the charset, and hence may not be equal to the

* length of the byte array.

*

* <p> The behavior of this constructor when the given bytes are not valid

* in the default charset is unspecified. The {@link

* java.nio.charset.CharsetDecoder} class should be used when more control

* over the decoding process is required.

*

* @param bytes

* The bytes to be decoded into characters

*

* @since JDK1.1

*

* @diffblue.noSupport

*/

public String(byte bytes[]) {

CProver.notModelled();

// this(bytes, 0, bytes.length);

}

/**

* Allocates a new string that contains the sequence of characters

* currently contained in the string buffer argument. The contents of the

* string buffer are copied; subsequent modification of the string buffer

* does not affect the newly created string.

*

* @param buffer

* A {@code StringBuffer}

*

* @diffblue.noSupport

*/

public String(StringBuffer buffer) {

CProver.notModelled();

// synchronized(buffer) {

// this.value = Arrays.copyOf(buffer.getValue(), buffer.length());

// }

}

/**

* Allocates a new string that contains the sequence of characters

* currently contained in the string builder argument. The contents of the

* string builder are copied; subsequent modification of the string builder

* does not affect the newly created string.

*

* <p> This constructor is provided to ease migration to {@code

* StringBuilder}. Obtaining a string from a string builder via the {@code

* toString} method is likely to run faster and is generally preferred.

*

* @param builder

* A {@code StringBuilder}

*

* @since 1.5

*

* @diffblue.fullSupport

* @diffblue.untested

*/

public String(StringBuilder builder) {

// DIFFBLUE MODEL LIBRARY This is treated internally in CBMC

// this.value = Arrays.copyOf(builder.getValue(), builder.length());

}

/*

* Package private constructor which shares value array for speed.

* this constructor is always expected to be called with share==true.

* a separate constructor is needed because we already have a public

* String(char[]) constructor that makes a copy of the given char[].

*/

// DIFFBLUE MODEL LIBRARY Unused package private method

// String(char[] value, boolean share) {

// // assert share : "unshared not supported";

// this.value = value;

// }

/**

* Returns the length of this string.

* The length is equal to the number of <a href="Character.html#unicode">Unicode

* code units</a> in the string.

*

* @return the length of the sequence of characters represented by this

* object.

*

* @diffblue.fullSupport

* @diffblue.untested

*/

public int length() {

// DIFFBLUE MODEL LIBRARY This is treated internally in CBMC

// return value.length;

return CProver.nondetInt();

}

/**

* Returns {@code true} if, and only if, {@link #length()} is {@code 0}.

*

* @return {@code true} if {@link #length()} is {@code 0}, otherwise

* {@code false}

*

* @since 1.6

*

* @diffblue.fullSupport

* @diffblue.untested

*/

public boolean isEmpty() {

// DIFFBLUE MODEL LIBRARY This is treated internally in CBMC

// return value.length == 0;

return CProver.nondetBoolean();

}

/**

* Returns the {@code char} value at the

* specified index. An index ranges from {@code 0} to

* {@code length() - 1}. The first {@code char} value of the sequence

* is at index {@code 0}, the next at index {@code 1},

* and so on, as for array indexing.

*

* <p>If the {@code char} value specified by the index is a

* <a href="Character.html#unicode">surrogate</a>, the surrogate

* value is returned.

*

* @param index the index of the {@code char} value.

* @return the {@code char} value at the specified index of this string.

* The first {@code char} value is at index {@code 0}.

* @exception IndexOutOfBoundsException if the {@code index}

* argument is negative or not less than the length of this

* string.

*

* @diffblue.fullSupport

* @diffblue.untested

*/

public char charAt(int index) {

// DIFFBLUE MODEL LIBRARY

// Our implementation differs slightly from the original

// as we use the internal CProverString.charAt of CBMC,

// however the behavior is the same as the JDK version.

// if ((index < 0) || (index >= value.length)) {

// throw new StringIndexOutOfBoundsException(index);

// }

// return value[index];

if ((index < 0) || (index >= length())) {

throw new StringIndexOutOfBoundsException(index);

}

return CProverString.charAt(this, index);

}

/**

* Returns the character (Unicode code point) at the specified

* index. The index refers to {@code char} values

* (Unicode code units) and ranges from {@code 0} to

* {@link #length()}{@code - 1}.

*

* <p> If the {@code char} value specified at the given index

* is in the high-surrogate range, the following index is less

* than the length of this {@code String}, and the

* {@code char} value at the following index is in the

* low-surrogate range, then the supplementary code point

* corresponding to this surrogate pair is returned. Otherwise,

* the {@code char} value at the given index is returned.

*

* @param index the index to the {@code char} values

* @return the code point value of the character at the

* {@code index}

* @exception IndexOutOfBoundsException if the {@code index}

* argument is negative or not less than the length of this

* string.

* @since 1.5

*

* @diffblue.fullSupport

* @diffblue.untested Tests only cover exception throwing

*/

public int codePointAt(int index) {

if ((index < 0) || (index >= this.length())) {

throw new StringIndexOutOfBoundsException(index);

}

// return Character.codePointAtImpl(value, index, value.length);

return CProverString.codePointAt(this, index);

}

/**

* Returns the character (Unicode code point) before the specified

* index. The index refers to {@code char} values

* (Unicode code units) and ranges from {@code 1} to {@link

* CharSequence#length() length}.

*

* <p> If the {@code char} value at {@code (index - 1)}

* is in the low-surrogate range, {@code (index - 2)} is not

* negative, and the {@code char} value at {@code (index -

* 2)} is in the high-surrogate range, then the

* supplementary code point value of the surrogate pair is

* returned. If the {@code char} value at {@code index -

* 1} is an unpaired low-surrogate or a high-surrogate, the

* surrogate value is returned.

*

* @param index the index following the code point that should be returned

* @return the Unicode code point value before the given index.

* @exception IndexOutOfBoundsException if the {@code index}

* argument is less than 1 or greater than the length

* of this string.

* @since 1.5

*

* @diffblue.fullSupport

*/

public int codePointBefore(int index) {

int i = index - 1;

if ((i < 0) || (i >= this.length())) {

throw new StringIndexOutOfBoundsException(index);

}

// return Character.codePointBeforeImpl(value, index, 0);

return CProverString.codePointBefore(this, index);

}

/**

* Returns the number of Unicode code points in the specified text

* range of this {@code String}. The text range begins at the

* specified {@code beginIndex} and extends to the

* {@code char} at index {@code endIndex - 1}. Thus the

* length (in {@code char}s) of the text range is

* {@code endIndex-beginIndex}. Unpaired surrogates within

* the text range count as one code point each.

*

* @param beginIndex the index to the first {@code char} of

* the text range.

* @param endIndex the index after the last {@code char} of

* the text range.

* @return the number of Unicode code points in the specified text

* range

* @exception IndexOutOfBoundsException if the

* {@code beginIndex} is negative, or {@code endIndex}

* is larger than the length of this {@code String}, or

* {@code beginIndex} is larger than {@code endIndex}.

* @since 1.5

*

* @diffblue.limitedSupport

* The result of this function is approximated.

* @diffblue.untested Tests only cover exception throwing

*/

public int codePointCount(int beginIndex, int endIndex) {

if (beginIndex < 0 || endIndex > this.length() || beginIndex > endIndex) {

throw new IndexOutOfBoundsException();

}

// return Character.codePointCountImpl(value, beginIndex, endIndex - beginIndex);

return CProverString.codePointCount(this, beginIndex, endIndex);

}

/**

* Returns the index within this {@code String} that is

* offset from the given {@code index} by

* {@code codePointOffset} code points. Unpaired surrogates

* within the text range given by {@code index} and

* {@code codePointOffset} count as one code point each.

*

* @param index the index to be offset

* @param codePointOffset the offset in code points

* @return the index within this {@code String}

* @exception IndexOutOfBoundsException if {@code index}

* is negative or larger then the length of this

* {@code String}, or if {@code codePointOffset} is positive

* and the substring starting with {@code index} has fewer

* than {@code codePointOffset} code points,

* or if {@code codePointOffset} is negative and the substring

* before {@code index} has fewer than the absolute value

* of {@code codePointOffset} code points.

* @since 1.5

*

* @diffblue.limitedSupport

* The result of this function is approximated. Only the

* {@code IndexOutOfBoundsException} related to {@code index} is thrown.

* @diffblue.untested Only exception throwing is tested.

*/

public int offsetByCodePoints(int index, int codePointOffset) {

if (index < 0 || index > this.length()) {

throw new IndexOutOfBoundsException();

}

// return Character.offsetByCodePointsImpl(value, 0, value.length,

// index, codePointOffset);

return CProverString.offsetByCodePoints(this, index, codePointOffset);

}

/**

* Copy characters from this string into dst starting at dstBegin.

* This method doesn't perform any range checking.

*/

// DIFFBLUE MODEL LIBRARY Unused private method

// void getChars(char dst[], int dstBegin) {

// System.arraycopy(value, 0, dst, dstBegin, value.length);

// }

/**

* Copies characters from this string into the destination character

* array.

* <p>

* The first character to be copied is at index {@code srcBegin};

* the last character to be copied is at index {@code srcEnd-1}

* (thus the total number of characters to be copied is

* {@code srcEnd-srcBegin}). The characters are copied into the

* subarray of {@code dst} starting at index {@code dstBegin}

* and ending at index:

* <blockquote><pre>

* dstbegin + (srcEnd-srcBegin) - 1

* </pre></blockquote>

*

* @param srcBegin index of the first character in the string

* to copy.

* @param srcEnd index after the last character in the string

* to copy.

* @param dst the destination array.

* @param dstBegin the start offset in the destination array.

* @exception IndexOutOfBoundsException If any of the following

* is true:

* <ul><li>{@code srcBegin} is negative.

* <li>{@code srcBegin} is greater than {@code srcEnd}

* <li>{@code srcEnd} is greater than the length of this

* string

* <li>{@code dstBegin} is negative

* <li>{@code dstBegin+(srcEnd-srcBegin)} is larger than

* {@code dst.length}</ul>

*

* @diffblue.noSupport

*/

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

// }

// System.arraycopy(value, srcBegin, dst, dstBegin, srcEnd - srcBegin);

}

/**

* Copies characters from this string into the destination byte array. Each

* byte receives the 8 low-order bits of the corresponding character. The

* eight high-order bits of each character are not copied and do not

* participate in the transfer in any way.

*

* <p> The first character to be copied is at index {@code srcBegin}; the

* last character to be copied is at index {@code srcEnd-1}. The total

* number of characters to be copied is {@code srcEnd-srcBegin}. The

* characters, converted to bytes, are copied into the subarray of {@code

* dst} starting at index {@code dstBegin} and ending at index:

*

* <blockquote><pre>

* dstbegin + (srcEnd-srcBegin) - 1

* </pre></blockquote>

*

* @deprecated This method does not properly convert characters into

* bytes. As of JDK&nbsp;1.1, the preferred way to do this is via the

* {@link #getBytes()} method, which uses the platform's default charset.

*

* @param srcBegin

* Index of the first character in the string to copy

*

* @param srcEnd

* Index after the last character in the string to copy

*

* @param dst

* The destination array

*

* @param dstBegin

* The start offset in the destination array

*

* @throws IndexOutOfBoundsException

* If any of the following is true:

* <ul>

* <li> {@code srcBegin} is negative

* <li> {@code srcBegin} is greater than {@code srcEnd}

* <li> {@code srcEnd} is greater than the length of this String

* <li> {@code dstBegin} is negative

* <li> {@code dstBegin+(srcEnd-srcBegin)} is larger than {@code

* dst.length}

* </ul>

*

* @diffblue.noSupport

*/

@Deprecated

public void getBytes(int srcBegin, int srcEnd, byte 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);

// }

// Objects.requireNonNull(dst);

//

// int j = dstBegin;

// int n = srcEnd;

// int i = srcBegin;

// char[] val = value; /* avoid getfield opcode */

//

// while (i < n) {

// dst[j++] = (byte)val[i++];

// }

}

/**