Test for printing double values in trace

This checks a limit double value is printed with sufficient
precision (the decimal version would not work so we have to use the hexidecimal).

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