Merge pull request #4700 from forejtv/forejtv/float-zero

Float 0 to string implementation

Author: Vojtěch Forejt

jbmc/regression/jbmc-strings/float-to-string/Test.class

@@ -0,0 +1,15 @@
+public class Test {
+
+    static void checkStringInputValue(float f) {
+      String s = Float.toString(f);
+      // the 1/f is needed to distinguish -0 from 0, '==' disregards the
+      // difference, while the division yields +Infinity or -Infinity.
+      if (f == 0.0f && 1/f > 0) {
+        assert(s.equals("0.0"));
+      } else if (f == -0.0f && 1/f < 0) {
+        assert(s.equals("-0.0"));
+      } else if (f == 1.0f ) {
+        assert(s.equals("1.0"));
+      }
+    }
+}

jbmc/regression/jbmc-strings/float-to-string/Test.java

@@ -0,0 +1,8 @@
+CORE
+Test.class
+--function Test.checkStringInputValue --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+^EXIT=0$
+^SIGNAL=0$
+assertion.1.*SUCCESS
+assertion.2.*SUCCESS
+assertion.3.*SUCCESS

jbmc/regression/jbmc-strings/float-to-string/test2.desc

@@ -950,6 +950,22 @@ code_blockt java_string_library_preprocesst::make_float_to_string_code(
     string_literal_to_string_expr("-Infinity", loc, symbol_table, code);
   string_expr_list.push_back(minus_infinity);
 
+  // Case of 0.0
+  // Note: for zeros we must use equal_exprt and not ieee_float_equal_exprt,
+  // the latter disregards the sign
+  condition_list.push_back(equal_exprt(arg, zero));
+  const refined_string_exprt zero_string =
+    string_literal_to_string_expr("0.0", loc, symbol_table, code);
+  string_expr_list.push_back(zero_string);
+
+  // Case of -0.0
+  ieee_floatt minus_zero_float(float_spec);
+  minus_zero_float.from_float(-0.0f);
+  condition_list.push_back(equal_exprt(arg, minus_zero_float.to_expr()));
+  const refined_string_exprt minus_zero_string =
+    string_literal_to_string_expr("-0.0", loc, symbol_table, code);
+  string_expr_list.push_back(minus_zero_string);
+
   // Case of simple notation
   ieee_floatt bound_inf_float(float_spec);
   ieee_floatt bound_sup_float(float_spec);