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,47 @@ 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;
+
+        // All primitive types are cast to a long
+        long longValue = 0;
+        if(obj instanceof Integer) {
+            longValue = (Integer) obj;
+        } else if(obj instanceof Long) {
+            longValue = (Long) obj;
+        } else if(obj instanceof Float) {
+            longValue = (long) ((Float)obj).doubleValue();
+        } else if (obj instanceof Double) {
+            longValue = (long) ((Double)obj).doubleValue();
+        } else if (obj instanceof Character) {
+            char charValue = (Character)obj;
+            longValue = (long) charValue;
+        } else if(obj instanceof Byte) {
+            byte byteValue = ((Byte)obj);
+            longValue = (long) byteValue;
+        } else if(obj instanceof Boolean) {
+            longValue = ((Boolean) obj) ? 1 : 0;
+        }
+
+        // The long value is encoded using a string of 4 characters
+        char array[] = {
+                (char) (longValue >> 48 & 0xFFFF),
+                (char) (longValue >> 32 & 0xFFFF),
+                (char) (longValue >> 16 & 0xFFFF),
+                (char) (longValue & 0xFFFF)};
+        return new String(array);
+    }
+
     /**
      * Returns a formatted string using the specified format string and
      * arguments.
@@ -3946,9 +3987,23 @@ 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();
+        if(args.length > 10) {
+            return CProver.nondetWithoutNull("");
+        }
+        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);
     }
 
     /**