Add a model of String.format

This uses CProverString.format which is builtin in the string solver.

Author: romainbrenguier

src/main/java/java/lang/String.java

@@ -3750,6 +3750,34 @@ public char[] toCharArray() {
         return result;
     }
 
+    /**
+     * Helper function for the {@code format} function.
+     * Serialize potential String.format argument to a String.
+     * The returned String is never null.
+     */
+    static String cproverFormatArgument(Object obj)
+    {
+        if(obj == null)
+            return "";
+        if(obj instanceof String)
+            return (String)obj;
+        if(obj instanceof Integer)
+            return Integer.toHexString((Integer)obj);
+        if(obj instanceof Character)
+            return String.valueOf(((Character) obj).charValue());
+        if(obj instanceof Byte)
+            return Integer.toHexString(((Byte) obj).intValue());
+        if(obj instanceof Long)
+            return Long.toHexString((Long) obj);
+        if(obj instanceof Boolean)
+            return ((Boolean) obj) ? "true" : "false";
+        if(obj instanceof Float)
+            return Integer.toHexString((int)((Float) obj).floatValue());
+        if(obj instanceof Double)
+            return Long.toHexString((long)((Float) obj).floatValue());
+        return "";
+    }
+
     /**
      * Returns a formatted string using the specified format string and
      * arguments.
@@ -3812,9 +3840,20 @@ public char[] toCharArray() {
      * @diffblue.untested
      */
     public static String format(String format, Object... args) {
-        // DIFFBLUE MODEL LIBRARY This is treated internally in CBMC
-        return CProver.nondetWithoutNullForNotModelled();
+        // DIFFBLUE MODEL LIBRARY
         // return new Formatter().format(format, args).toString();
+        String arg1 = args.length > 0 ? cproverFormatArgument(args[0]) : "";
+        String arg2 = args.length > 1 ? cproverFormatArgument(args[1]) : "";
+        String arg3 = args.length > 2 ? cproverFormatArgument(args[2]) : "";
+        String arg4 = args.length > 3 ? cproverFormatArgument(args[3]) : "";
+        String arg5 = args.length > 4 ? cproverFormatArgument(args[4]) : "";
+        String arg6 = args.length > 5 ? cproverFormatArgument(args[5]) : "";
+        String arg7 = args.length > 6 ? cproverFormatArgument(args[6]) : "";
+        String arg8 = args.length > 7 ? cproverFormatArgument(args[7]) : "";
+        String arg9 = args.length > 8 ? cproverFormatArgument(args[8]) : "";
+        String arg10 = args.length > 9 ? cproverFormatArgument(args[9]) : "";
+        return CProverString.format(format, arg1, arg2, arg3, arg4, arg5, arg6,
+                arg7, arg8, arg9, arg10);
     }
 
     /**