Adding tests for String.valueOf float

Add several tests, some take long and are marked as THOROUGH, fail
probably due to some problem in CBMC and are marked as KNOWNBUG.

Author: romainbrenguier

regression/strings-smoke-tests/java_value_of_float_2/test.class

@@ -0,0 +1,8 @@
+KNOWNBUG
+test.class
+--refine-strings --function test.check
+^EXIT=10$
+^SIGNAL=0$
+assertion.* file test.java line 6 .* SUCCESS$
+assertion.* file test.java line 7 .* FAILURE$
+--

regression/strings-smoke-tests/java_value_of_float_2/test.desc

@@ -0,0 +1,9 @@
+public class test
+{
+    public static void check()
+    {
+        String s3=String.valueOf(7.89e12f);
+        assert(s3.equals("7.89E12"));
+        assert(!s3.equals("7.89E12"));
+    }
+}

regression/strings-smoke-tests/java_value_of_float_2/test.java

@@ -0,0 +1,9 @@
+KNOWNBUG
+test.class
+--refine-strings --function test.check
+^EXIT=10$
+^SIGNAL=0$
+assertion.* file test.java line 7 .* SUCCESS$
+assertion.* file test.java line 8 .* FAILURE$
+
+--

regression/strings-smoke-tests/java_value_of_float_3/test.class

@@ -0,0 +1,10 @@
+public class test
+{
+    public static void check()
+    {
+        String s5=String.valueOf(5.67e-9f);
+        // The result may not be exactly 5.67E-9 as 5.66999...E-9 is also valid
+        assert(s5.startsWith("5.6") && s5.endsWith("E-9"));
+        assert(!s5.startsWith("5.6") || !s5.endsWith("E-9"));
+    }
+ }

regression/strings-smoke-tests/java_value_of_float_3/test.desc

@@ -0,0 +1,10 @@
+THOROUGH
+test.class
+--refine-strings --function test.check
+^EXIT=10$
+^SIGNAL=0$
+assertion.* test.java line 8 .* SUCCESS$
+assertion.* test.java line 9 .* SUCCESS$
+assertion.* test.java line 10 .* SUCCESS$
+assertion.* test.java line 11 .* FAILURE$
+--

regression/strings-smoke-tests/java_value_of_float_3/test.java

@@ -0,0 +1,13 @@
+public class test
+{
+    public static void check()
+    {
+        String s7=String.valueOf(java.lang.Float.POSITIVE_INFINITY);
+        String s8=String.valueOf(java.lang.Float.NEGATIVE_INFINITY);
+        String s9=String.valueOf(java.lang.Float.NaN);
+        assert(s7.equals("Infinity"));
+        assert(s8.equals("-Infinity"));
+        assert(s9.equals("NaN"));
+        assert(!s7.equals("Infinity") || !s8.equals("-Infinity") || !s9.equals("NaN"));
+    }
+}

regression/strings-smoke-tests/java_value_of_float_4/test.class

@@ -0,0 +1,8 @@
+THOROUGH
+test.class
+--refine-strings --function test.check
+^EXIT=10$
+^SIGNAL=0$
+assertion.* file test.java line 6 .* SUCCESS$
+assertion.* file test.java line 7 .* FAILURE$
+--

regression/strings-smoke-tests/java_value_of_float_4/test.desc

@@ -0,0 +1,9 @@
+public class test
+{
+    public static void check()
+    {
+        String s1=String.valueOf(-123.456f);
+        assert(s1.equals("-123.456"));
+        assert(!s1.equals("-123.456"));
+    }
+}