Refactor conversions from primitive types to String

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

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<Byte> {
      * @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);
     }
 
     /**

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

src/main/java/java/lang/Double.java

@@ -208,11 +208,14 @@ public final class Double extends Number implements Comparable<Double> {
      *
      * @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);
     }
 
     /**

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<Float> {
      *
      * @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);
     }
 
     /**

src/main/java/java/lang/Integer.java

@@ -119,10 +119,11 @@ public final class Integer extends Number implements Comparable<Integer> {
      * @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&nbsp;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);
     }
 
     /**

src/main/java/java/lang/Long.java

@@ -123,9 +123,11 @@ public final class Long extends Number implements Comparable<Long> {
      * @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&nbsp;10.
+     *
+     * @diffblue.fullSupport
      */
     public static String toString(long i) {
-         // this function is handled by cbmc internally
-        return CProver.nondetWithoutNullForNotModelled();
+        return CProverString.toString(i);
     }
 
     /**

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<Short> {
      * @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);
     }
 
     /**

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

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