Implement toString() methods of box types using CProverString methods

Author: danpoe

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