Merge pull request diffblue#4498 from romainbrenguier/bugfix/double-printing

Fix bug in the printing of double for limit values

Author: romainbrenguier

jbmc/regression/jbmc/double1/double1.class

@@ -19,5 +19,13 @@ public static void main(String[] args)
     d=java.lang.Double.NEGATIVE_INFINITY;
     d=java.lang.Double.NaN;
   }
+
+  public static String testLimit(double inputValue) {
+    if(0x1p-1022 == inputValue){
+      assert(false);
+      return "reach";
+    }
+    return "default";
+  }
 }
 

jbmc/regression/jbmc/double1/double1.java

@@ -0,0 +1,11 @@
+CORE
+double1.class
+ --function double1.testLimit --trace
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+INPUT arg0d: 0x1(\.0*)?p-1022 /\* 2.22507e-308
+--
+^warning: ignoring
+--
+Test double value are printed with sufficient precision

jbmc/regression/jbmc/double1/test-limit.desc

@@ -79,8 +79,6 @@ std::string floating_point_to_java_string(float_type value)
     return raw_decimal;
   }();
   const bool is_lossless = [&] {
-    if(value == std::numeric_limits<float_type>::min())
-      return true;
     try
     {
       return std::stod(decimal) == value;