From ca20b14ea370b2919bb00a41586cae2fd74b4c09 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Mon, 8 Apr 2019 16:09:01 +0100
Subject: [PATCH 1/2] Remove special case of limit for double printing

The case of numeric limit for floating point does not imply that the
decimal version is precise enough.
An example of that is 0x1p-1022 which would be printed as 2.22507e-308
in decimal but this is not precise enough.
---
 jbmc/src/java_bytecode/expr2java.h | 2 --
 1 file changed, 2 deletions(-)

diff --git a/jbmc/src/java_bytecode/expr2java.h b/jbmc/src/java_bytecode/expr2java.h
index a602b612a44..42339ff8782 100644
--- a/jbmc/src/java_bytecode/expr2java.h
+++ b/jbmc/src/java_bytecode/expr2java.h
@@ -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;

From edfccab4cff58c82698e45218a442e9c532aa0b5 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Mon, 8 Apr 2019 13:13:16 +0100
Subject: [PATCH 2/2] 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).
---
 jbmc/regression/jbmc/double1/double1.class   | Bin 470 -> 883 bytes
 jbmc/regression/jbmc/double1/double1.java    |   8 ++++++++
 jbmc/regression/jbmc/double1/test-limit.desc |  11 +++++++++++
 3 files changed, 19 insertions(+)
 create mode 100644 jbmc/regression/jbmc/double1/test-limit.desc

diff --git a/jbmc/regression/jbmc/double1/double1.class b/jbmc/regression/jbmc/double1/double1.class
index e96fdb5e5134bdf3607ef187a6ba2a7ef85faae7..7d62e4f55b9f7ec892d3d75532f63fea3cf87bac 100644
GIT binary patch
literal 883
zcmZWnT~8B16g|^+ciUybvRz86;3w7vw3S**6`~l522wS##sqv?x+5;OTeIC76Cd~o
z)#!r>f52DN1QJQ~-9Mwg>5F=2+d_<+%*@?;XU;kI%zXX*=`(-==2WC%Dwve$SA0_{
zLfvUvzW(EvcWbHiO~HA2>wC8@|LF%?KYJO(yFm=2xS$}bA^|gsToe}-%&5rYl7a$5
zV!~>*xaT`fw^epp)_R@W3~Y@-o_Acwzs3+YCm%3G7MnI_I8t$3ey817=iYs>nF<Zd
zaT${4!^)=h%*xd*cOzHzJ;&Xc69;2HZ}}Cc;rI+AW_j}eT?~U&->N;iZ9VN_M(1nw
z9=lp?w!Ip^=?E^(ZnlYZCM%dUjA5K19<a83r=GiKxpuQ5@|QIfG21T&lFGqR4M%Z|
zA$2JAM!)|h&ue-NlE<yuV+O_MkF0i`R4YAJ1tkqvaP=S9yX%|0Mw=q$is)8#`E$QZ
z6*yNW%MQ5~>*O|hW%HKfar=Op+V|U3AgkAKlCCUGx5wfsA(o;D4eAvP$0-skqg9&P
z1A9*a!wH(@AW41`z$uEw))#bCrFC{6p;ZInJxG=5UC7I3rx-CiuZxoTa#l89m7-?n
zO)+LbSvH{3&}a-TAA;wh5sZWZDD<*a7!;)`H;zFf8$t%dn1YThJ+nMjix?pxr*Wny
zWQBx;2w}`XJo9!N#s}!z7}!T*bq~fDePl;Z?od4xw4w(crw}EMBzcgg?kA{97|9T2
q&mMSD2$}|l_0e6VwxLAcArk%wT}bbO^?eZl5<=R7a4!>-&;13a{G&Yp

delta 241
zcmey&c8yu@)W2Q(7#J9g7?ije1Q;aQ8KhW&ToBOWVqjvB1`#rB_8)&1xw~4tpJ*t}
z#?Bzi&LB6j*UOD7IKQ+gIn^yQCzX+bCndi$DJRuXFDtPuk%vK$L5Pt-0L0cWEy>K$
z4@%5S$<GCe%kwZOFeoxIutPOWUdgEI2o&N6+7ALuKn&E)z{nsBWXS?)Mj*|qwVi=+
zBap$!AOa-Wz=DhnoD8B2VnDX=<NziMK~7H*25unc^@OUNJd??slaWCjsDp_?0sta+
BD69Yg

diff --git a/jbmc/regression/jbmc/double1/double1.java b/jbmc/regression/jbmc/double1/double1.java
index f71435b7641..23d93024d5e 100644
--- a/jbmc/regression/jbmc/double1/double1.java
+++ b/jbmc/regression/jbmc/double1/double1.java
@@ -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";
+  }
 }
 
diff --git a/jbmc/regression/jbmc/double1/test-limit.desc b/jbmc/regression/jbmc/double1/test-limit.desc
new file mode 100644
index 00000000000..cd8817af619
--- /dev/null
+++ b/jbmc/regression/jbmc/double1/test-limit.desc
@@ -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