/*

* 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

*/

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

*/

public String(String original) {

// DIFFBLUE MODEL LIBRARY This is treated internally in CBMC

// this.value = original.value;

// this.hash = original.hash;

}

/**

* Intermediary function for modelling the constructor String(char value[]).

*/

private static String CProverStringOfCharArray(char value[]) {

if (value == null) {

throw new NullPointerException();

}

return CProverString.ofCharArray(value, 0, value.length);

}

/**

* 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.limitedSupport

* The length of the String constructed is limited by the unwind

* parameter.

*/

public String(char value[]) {

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

// DIFFBLUE MODEL LIBRARY

this(CProverStringOfCharArray(value));

}

/**

* 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

* 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

* @diffblue.untested

*/

public String(char value[], int offset, int count) {

// DIFFBLUE MODEL LIBRARY

this(CProverStringOfCharArray(value, 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);

// }

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

}

/**

* DIFFBLUE MODEL LIBRARY

* Helper for generating non-deterministic strings.

*/

private static String cproverNonDet()

{

return CProver.nondetWithoutNull("");

}

/**

* 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.limitedSupport

* Assumes all codePoints are in the Basic Multilingual Plane.

* An implication of this limitation is that no trace is generated for

* the cases where IllegalArgumentException would be thrown.

*/

public String(int[] codePoints, 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 > 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;

// DIFFBLUE MODEL LIBRARY

// We initialize the string non-deterministically and add constraints on

// it, instead of using an array of characters.

this(cproverNonDet());

if (offset < 0) {

throw new StringIndexOutOfBoundsException(offset);

}

if (count < 0) {

throw new StringIndexOutOfBoundsException(count);

}

if (offset > codePoints.length - count) {

throw new StringIndexOutOfBoundsException(offset + count);

}

final int end = offset + count;

CProver.assume(length() == count);

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

int c = codePoints[i];

CProver.assume(Character.isBmpCodePoint(c));

CProver.assume(CProverString.charAt(this, j) == (char)c);

}

}

/**

* 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.limitedSupport

* The length of the String constructed is limited by the unwind

* parameter.

*/

@Deprecated

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

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

// DIFFBLUE MODEL LIBRARY

// We initialize the string non-deterministically and add constraints on

// it, instead of using an array of characters.

this(cproverNonDet());

checkBounds(ascii, offset, count);

CProver.assume(length() == count);

if (hibyte == 0) {

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

CProver.assume(CProverString.charAt(this, i) == (char)(ascii[i + offset] & 0xff));

}

} else {

hibyte <<= 8;

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

CProver.assume(CProverString.charAt(this, i) == (char)(hibyte | (ascii[i + offset] & 0xff)));

}

}

}

/**

* 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.limitedSupport

* The length of the String constructed is limited by the unwind

* parameter.

*/

@Deprecated

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

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.

*/

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.limitedSupport

* The length of the String constructed is limited by the unwind

* parameter.

*/

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

throws UnsupportedEncodingException {

// if (charsetName == null)

// throw new NullPointerException("charsetName");

// checkBounds(bytes, offset, length);

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

// DIFFBLUE MODEL LIBRARY

// We initialize the string non-deterministically and add constraints on

// it, instead of using an array of characters.

this(cproverNonDet());

if (charsetName == null)

throw new NullPointerException("charsetName");

checkBounds(bytes, offset, length);

byte[] getBytesResult = cproverReversibleGetBytes(charsetName);

CProver.assume(getBytesResult.length == length);

for (int i = 0; i < length; i++) {

CProver.assume(bytes[i + offset] == getBytesResult[i]);

}

}

/**

* 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.limitedSupport

* The length of the String constructed is limited by the unwind

* parameter.

*/

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

{

// if (charset == null)

// throw new NullPointerException("charset");

// checkBounds(bytes, offset, length);

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

// DIFFBLUE MODEL LIBRARY

// We initialize the string non-deterministically and add constraints on

// it, instead of using an array of characters.

this(cproverNonDet());

if (charset == null)

throw new NullPointerException("charset");

checkBounds(bytes, offset, length);

byte[] getBytesResult = cproverReversibleGetBytes(charset);

CProver.assume(getBytesResult.length == length);

for (int i = 0; i < length; i++) {

CProver.assume(bytes[i + offset] == getBytesResult[i]);

}

}

/**

* 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.limitedSupport

* The length of the String constructed is limited by the unwind

* parameter.

*/

public String(byte bytes[], String charsetName)

throws UnsupportedEncodingException {

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

}

/**

* DIFFBLUE MODEL LIBRARY

* Used to construct a string from a byte array and a charset.

*

* It does so by generating a non-deterministic string `s` and assuming

* `bytes` is equal to the result of `s.getBytes(charset)`.

*

* @param bytes

* The bytes to be decoded into characters

*

* @param charset

* a supported {@linkplain java.nio.charset.Charset charset}

*

* @return the constructed string

*/

private static String cproverOfByteArray(byte[] bytes, Charset charset)

{

String s = CProver.nondetWithoutNull("");

byte[] getBytesResult = s.cproverReversibleGetBytes(charset);

CProver.assume(getBytesResult.length == bytes.length);

for (int i = 0; i < bytes.length; i++) {

CProver.assume(bytes[i] == getBytesResult[i]);

}

return s;

}

/**

* 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.limitedSupport

* Only standard charsets are supported and for ASCII, UTF-8 and ISO-8859-1

* we restrict all the characters to be ASCII.

*/

public String(byte bytes[], Charset charset)

{

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

// DIFFBLUE MODEL LIBRARY

this(cproverOfByteArray(bytes, 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.limitedSupport We assume all the bytes are ASCII characters,

* and that the default charset encodes ASCII characters with one byte.

*/

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

// DIFFBLUE MODEL LIBRARY

// We initialize the string non-deterministically and add constraints on

// it, instead of using an array of characters.

this(cproverNonDet());

checkBounds(bytes, offset, length);

// DIFFBLUE MODEL LIBRARY We replace StringCoding.decode by the implementation below

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

CProver.assume(length() == length);

byte[] getBytesResult = cproverGetBytesEnforceAscii();

CProver.assume(getBytesResult.length == length);

for (int i = 0; i < length; i++) {

CProver.assume(bytes[i + offset] == getBytesResult[i]);

}

}

/**

* 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.limitedSupport We assume all the bytes are ASCII characters,

* and that the default charset encodes ASCII characters with one byte.

*/

public String(byte bytes[]) {

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.fullSupport

*/

public String(StringBuffer buffer) {

this(buffer.toString());

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

}