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

@@ -3884,6 +3884,59 @@ 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)
+        {
+            int intValue = (Integer)obj;
+            // Fixed width translation
+            String result = cproverNonDet();
+            CProver.assume(result.length() == 4);
+            CProver.assume(CProverString.charAt(result, 0) == (char) 0);
+            CProver.assume(CProverString.charAt(result, 0) == (char) 0);
+            CProver.assume(CProverString.charAt(result, 2) == (char) (intValue & 0xFFFF));
+            CProver.assume(CProverString.charAt(result, 3) == (char) (intValue & 0xFFFF));
+            return result;
+        }
+        if(obj instanceof Character)
+            return String.valueOf(((Character) obj).charValue());
+        if(obj instanceof Byte)
+            return String.valueOf((char)((Byte) obj).byteValue());
+        if(obj instanceof Long) {
+            long longValue = (Long) obj;
+            // Fixed width translation
+            // Fixed width translation
+            String result = cproverNonDet();
+            CProver.assume(result.length() == 4);
+            CProver.assume(CProverString.charAt(result, 0) == (char) 0);
+            CProver.assume(CProverString.charAt(result, 0) == (char) 0);
+            CProver.assume(CProverString.charAt(result, 2) == (char) (longValue & 0xFFFF));
+            CProver.assume(CProverString.charAt(result, 3) == (char) (longValue & 0xFFFF));
+            return result;
+        }
+        if(obj instanceof Boolean)
+            return ((Boolean) obj) ? "true" : "false";
+        if(obj instanceof Float || obj instanceof Double) {
+            double doubleValue = obj instanceof Float
+                    ? ((Float)obj).doubleValue() :(Double) obj;
+            // Fixed width translation
+            char charArray[] = {
+                    (char) ((long)doubleValue >> 24), (char) ((long)doubleValue >> 16 & 0xFFFF),
+                    (char) ((long)doubleValue >> 8 & 0xFFFF), (char) ((long)doubleValue & 0xFFFF)};
+            return new String(charArray);
+        }
+        return "";
+    }
+
     /**
      * Returns a formatted string using the specified format string and
      * arguments.
@@ -3946,9 +3999,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);
     }
 
     /**