diff --git a/src/main/java/java/lang/Boolean.java b/src/main/java/java/lang/Boolean.java index fee8ae1..45e29b7 100644 --- a/src/main/java/java/lang/Boolean.java +++ b/src/main/java/java/lang/Boolean.java @@ -176,6 +176,8 @@ public static Boolean valueOf(String s) { * @param b the boolean to be converted * @return the string representation of the specified {@code boolean} * @since 1.4 + * + * @diffblue.fullSupport */ public static String toString(boolean b) { return b ? "true" : "false"; diff --git a/src/main/java/java/lang/Byte.java b/src/main/java/java/lang/Byte.java index 5901176..f11261c 100644 --- a/src/main/java/java/lang/Byte.java +++ b/src/main/java/java/lang/Byte.java @@ -26,6 +26,7 @@ package java.lang; import org.cprover.CProver; +import org.cprover.CProverString; /** * @@ -71,9 +72,11 @@ public final class Byte extends Number implements Comparable { * @param b the {@code byte} to be converted * @return the string representation of the specified {@code byte} * @see java.lang.Integer#toString(int) + * + * @diffblue.fullSupport */ public static String toString(byte b) { - return Integer.toString((int)b, 10); + return CProverString.toString((int)b); } /** diff --git a/src/main/java/java/lang/Character.java b/src/main/java/java/lang/Character.java index 75a15f7..4d19da5 100644 --- a/src/main/java/java/lang/Character.java +++ b/src/main/java/java/lang/Character.java @@ -31,6 +31,7 @@ import java.util.Locale; import org.cprover.CProver; +import org.cprover.CProverString; /** * The {@code Character} class wraps a value of the primitive @@ -4651,9 +4652,12 @@ public String toString() { * @param c the {@code char} to be converted * @return the string representation of the specified {@code char} * @since 1.4 + * + * @diffblue.fullSupport */ public static String toString(char c) { - return String.valueOf(c); + char data[] = {c}; + return CProverString.ofCharArray(data, 0, 1); } /** diff --git a/src/main/java/java/lang/Double.java b/src/main/java/java/lang/Double.java index 2bb0975..037d557 100644 --- a/src/main/java/java/lang/Double.java +++ b/src/main/java/java/lang/Double.java @@ -208,11 +208,14 @@ public final class Double extends Number implements Comparable { * * @param d the {@code double} to be converted. * @return a string representation of the argument. - * @diffblue.noSupport + * + * @diffblue.limitedSupport + * The precision in the produced string may not match that of the + * actual program. */ public static String toString(double d) { // return FloatingDecimal.toJavaFormatString(d); - return String.valueOf(d); + return CProverString.toString(d); } /** diff --git a/src/main/java/java/lang/Float.java b/src/main/java/java/lang/Float.java index 1003bcc..452bb87 100644 --- a/src/main/java/java/lang/Float.java +++ b/src/main/java/java/lang/Float.java @@ -31,6 +31,7 @@ import sun.misc.FloatConsts; import sun.misc.DoubleConsts; import org.cprover.CProver; +import org.cprover.CProverString; /** * The {@code Float} class wraps a value of primitive type @@ -204,14 +205,13 @@ public final class Float extends Number implements Comparable { * * @param f the float to be converted. * @return a string representation of the argument. - * @diffblue.noSupport + * + * @diffblue.limitedSupport + * The precision in the produced string may not match that of the + * actual program. */ public static String toString(float f) { - // DIFFBLUE MODEL LIBRARY - // removed for compatibility with Java 9 and newer - // return FloatingDecimal.toJavaFormatString(f); - CProver.notModelled(); - return CProver.nondetWithNullForNotModelled(); + return CProverString.toString(f); } /** diff --git a/src/main/java/java/lang/Integer.java b/src/main/java/java/lang/Integer.java index b24f974..cae3f90 100644 --- a/src/main/java/java/lang/Integer.java +++ b/src/main/java/java/lang/Integer.java @@ -119,10 +119,11 @@ public final class Integer extends Number implements Comparable { * @return a string representation of the argument in the specified radix. * @see java.lang.Character#MAX_RADIX * @see java.lang.Character#MIN_RADIX + * + * @diffblue.fullSupport */ - // DIFFBLUE MODEL LIBRARY: Handled internally by CBMC public static String toString(int i, int radix) { - return CProver.nondetWithoutNullForNotModelled(); + return CProverString.toString(i, radix); } /** @@ -287,11 +288,11 @@ public static String toBinaryString(int i) { * * @param i an integer to be converted. * @return a string representation of the argument in base 10. + * + * @diffblue.fullSupport */ - // DIFFBLUE MODEL LIBRARY: Handled internally by CBMC public static String toString(int i) { - // this function is handled by cbmc internally - return CProver.nondetWithoutNullForNotModelled(); + return CProverString.toString(i); } /** diff --git a/src/main/java/java/lang/Long.java b/src/main/java/java/lang/Long.java index 4cc5e3f..a960b18 100644 --- a/src/main/java/java/lang/Long.java +++ b/src/main/java/java/lang/Long.java @@ -123,9 +123,11 @@ public final class Long extends Number implements Comparable { * @return a string representation of the argument in the specified radix. * @see java.lang.Character#MAX_RADIX * @see java.lang.Character#MIN_RADIX + * + * @diffblue.fullSupport */ public static String toString(long i, int radix) { - return CProver.nondetWithoutNullForNotModelled(); + return CProverString.toString(i, radix); } /** @@ -349,10 +351,11 @@ static String toUnsignedString0(long val, int shift) { * * @param i a {@code long} to be converted. * @return a string representation of the argument in base 10. + * + * @diffblue.fullSupport */ public static String toString(long i) { - // this function is handled by cbmc internally - return CProver.nondetWithoutNullForNotModelled(); + return CProverString.toString(i); } /** diff --git a/src/main/java/java/lang/Short.java b/src/main/java/java/lang/Short.java index a4a700d..1fd1a98 100644 --- a/src/main/java/java/lang/Short.java +++ b/src/main/java/java/lang/Short.java @@ -26,6 +26,7 @@ package java.lang; import org.cprover.CProver; +import org.cprover.CProverString; /** * The {@code Short} class wraps a value of primitive type {@code @@ -69,9 +70,11 @@ public final class Short extends Number implements Comparable { * @param s the {@code short} to be converted * @return the string representation of the specified {@code short} * @see java.lang.Integer#toString(int) + * + * @diffblue.fullSupport */ public static String toString(short s) { - return Integer.toString((int)s, 10); + return CProverString.toString((int)s); } /** diff --git a/src/main/java/java/lang/String.java b/src/main/java/java/lang/String.java index dd64c4a..390e734 100644 --- a/src/main/java/java/lang/String.java +++ b/src/main/java/java/lang/String.java @@ -4238,9 +4238,7 @@ public static String copyValueOf(char data[]) { * @diffblue.fullSupport */ public static String valueOf(boolean b) { - // DIFFBLUE MODEL LIBRARY This is treated internally in JBMC - return CProver.nondetWithoutNullForNotModelled(); - // return b ? "true" : "false"; + return b ? "true" : "false"; } /** @@ -4255,8 +4253,8 @@ public static String valueOf(boolean b) { * @diffblue.untested */ public static String valueOf(char c) { - // DIFFBLUE MODEL LIBRARY This is treated internally in CBMC - return CProver.nondetWithNullForNotModelled(); + char data[] = {c}; + return CProverString.ofCharArray(data, 0, 1); // char data[] = {c}; // return new String(data, true); } @@ -4275,8 +4273,7 @@ public static String valueOf(char c) { * @diffblue.untested */ public static String valueOf(int i) { - // DIFFBLUE MODEL LIBRARY This is treated internally in CBMC - return CProver.nondetWithoutNullForNotModelled(); + return CProverString.toString(i); // return Integer.toString(i); } @@ -4294,8 +4291,7 @@ public static String valueOf(int i) { * @diffblue.untested */ public static String valueOf(long l) { - // DIFFBLUE MODEL LIBRARY This is treated internally in CBMC - return CProver.nondetWithoutNullForNotModelled(); + return CProverString.toString(l); // return Long.toString(l); } @@ -4314,8 +4310,7 @@ public static String valueOf(long l) { * actual program. */ public static String valueOf(float f) { - // DIFFBLUE MODEL LIBRARY This is treated internally in CBMC - return CProver.nondetWithoutNullForNotModelled(); + return CProverString.toString(f); // return Float.toString(f); } @@ -4334,9 +4329,8 @@ public static String valueOf(float f) { * actual program. */ public static String valueOf(double d) { - // DIFFBLUE MODEL LIBRARY we cast the number down to float because // string solver only knows how to convert floats to string - return valueOf(CProver.doubleToFloat(d)); + return CProverString.toString(d); // return Double.toString(d); } diff --git a/src/main/java/org/cprover/CProverString.java b/src/main/java/org/cprover/CProverString.java index e7da071..c8dc4f6 100644 --- a/src/main/java/org/cprover/CProverString.java +++ b/src/main/java/org/cprover/CProverString.java @@ -348,4 +348,77 @@ public static String format( String arg4, String arg5, String arg6, String arg7, String arg8, String arg9) { return CProver.nondetWithoutNullForNotModelled(); } + + /** + * Returns a {@code String} object representing the + * specified integer. The argument is converted to signed decimal + * representation and returned as a string. + * + * @param i an integer to be converted. + * @return a string representation of the argument in base 10. + */ + public static String toString(int i) { + return CProver.nondetWithoutNullForNotModelled(); + } + + /** + * Returns a string representation of the first argument in the + * radix specified by the second argument. + * + * @param i an integer to be converted to a string. + * @param radix the radix to use in the string representation. + * @return a string representation of the argument in the specified radix. + */ + public static String toString(int i, int radix) { + return CProver.nondetWithoutNullForNotModelled(); + } + + /** + * Returns a {@code String} object representing the specified + * {@code long}. The argument is converted to signed decimal + * representation and returned as a string. + * + * @param l a {@code long} to be converted. + * @return a string representation of the argument in base 10. + */ + public static String toString(long l) { + return CProver.nondetWithoutNullForNotModelled(); + } + + /** + * Returns a string representation of the first argument in the + * radix specified by the second argument. + * + * @param l a {@code long} to be converted to a string. + * @param radix the radix to use in the string representation. + * @return a string representation of the argument in the specified radix. + */ + public static String toString(long l, int radix) { + return CProver.nondetWithoutNullForNotModelled(); + } + + /** + * Returns a string representation of the {@code float} + * argument. + * + * @param f the float to be converted. + * @return a string representation of the argument. + */ + public static String toString(float f) { + return CProver.nondetWithoutNullForNotModelled(); + } + + /** + * Returns a string representation of the {@code double} + * argument. + * + * The double is converted to a float first as the string solver currently + * can convert float to String but not double to String. + * + * @param d the double to be converted. + * @return a string representation of the argument. + */ + public static String toString(double d) { + return toString(CProver.doubleToFloat(d)); + } }