diff --git a/src/main/java/java/lang/String.java b/src/main/java/java/lang/String.java index e16dd1d..f38b3f8 100644 --- a/src/main/java/java/lang/String.java +++ b/src/main/java/java/lang/String.java @@ -4271,6 +4271,18 @@ public static String valueOf(double d) { // return Double.toString(d); } + /** + * Pool of strings used by the {@code String}.intern model. + */ + static String[] cproverInternPool = null; + + /** + * Number of elements stored in the pool for {@code String.intern} pool. + * This can be smaller than {@code cproverInternPool.length} which + * represents the capacity of the array and is fixed for each execution. + */ + static int cproverInternPoolSize = 0; + /** * Returns a canonical representation for the string object. *

@@ -4294,11 +4306,29 @@ public static String valueOf(double d) { * @return a string that has the same contents as this string, but is * guaranteed to be from a pool of unique strings. * - * @diffblue.noSupport + * @diffblue.limitedSupport literal strings and string-valued constant + * expressions are not interned. */ + // DIFFBLUE MODEL LIBRARY // public native String intern(); public String intern() { - CProver.notModelled(); - return CProver.nondetWithoutNullForNotModelled(); + // Initialize the pool if needed + if (cproverInternPool == null) { + int capacity = CProver.nondetInt(); + CProver.assume(capacity > 0); + cproverInternPool = new String[capacity]; + cproverInternPool[0] = this; + return this; + } + // Look for an entry in the pool equal to `this` + for (int i = 0; i < cproverInternPoolSize; ++i) { + if (CProverString.equals(cproverInternPool[i], this)) { + return cproverInternPool[i]; + } + } + // Add `this` to the pool + CProver.assume(cproverInternPool.length > cproverInternPoolSize); + cproverInternPool[cproverInternPoolSize++] = this; + return this; } }