Implement toString() methods of box types using CProverString methods

Author: danpoe

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
@@ -4653,7 +4654,8 @@ public String toString() {
      * @since 1.4
      */
     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

@@ -212,7 +212,7 @@ public final class Double extends Number implements Comparable<Double> {
      */
     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,9 @@ 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
      */
     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

@@ -120,9 +120,8 @@ public final class Integer extends Number implements Comparable<Integer> {
      * @see     java.lang.Character#MAX_RADIX
      * @see     java.lang.Character#MIN_RADIX
      */
-    // DIFFBLUE MODEL LIBRARY: Handled internally by CBMC
     public static String toString(int i, int radix) {
-        return CProver.nondetWithoutNullForNotModelled();
+        return CProverString.toString(i, radix);
     }
 
     /**
@@ -288,10 +287,8 @@ 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 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

@@ -125,7 +125,7 @@ public final class Long extends Number implements Comparable<Long> {
      * @see     java.lang.Character#MIN_RADIX
      */
     public static String toString(long i, int radix) {
-        return CProver.nondetWithoutNullForNotModelled();
+        return CProverString.toString(i, radix);
     }
 
     /**
@@ -351,8 +351,7 @@ static String toUnsignedString0(long val, int shift) {
      * @return  a string representation of the argument in base&nbsp;10.
      */
     public static String toString(long i) {
-         // this function is handled by cbmc internally
-        return CProver.nondetWithoutNullForNotModelled();
+        return CProverString.toString(i);
     }
 
     /**