Add test for String.format with float

This checks that having a format flag with precision defined doesn't
crash the solver.

Author: romainbrenguier

jbmc/regression/jbmc-strings/StringFormat/Test.class

@@ -49,4 +49,14 @@ public static String string3(String s, String t) {
     assert(s.length() != 1 || u.charAt(0) == u.charAt(u.length() - 1));
     return u;
   }
+
+  public static String float1(float f) {
+    String u = String.format("Pi is %.2f.", 3.14);
+    // We are not checking the exactness of the string produced, just that
+    // the solver will not crash.
+    assert(u.length() > 0);
+    assert(u.charAt(0) == 'P');
+    return u;
+  }
+
 }

jbmc/regression/jbmc-strings/StringFormat/Test.java

@@ -0,0 +1,6 @@
+CORE
+Test.class
+--function Test.float1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^EXIT=0$
+^SIGNAL=0$
+