java-semantics icon indicating copy to clipboard operation
java-semantics copied to clipboard

wrong precision for floats

Open rschumi0 opened this issue 4 years ago • 0 comments

Some of my tests showed that K-Java has a wrong precision for float values. I assume that float values were just encoded as double precision values. As a result, I could observe that in some calculations, K-Java produces results that significantly diverge from the results of Java. Moreover, K-Java sometimes produces a concrete value, whereas Java returns Infinity, which is shown in the following example:

float a = (float) 1 - 1473150328275393513L / 0.16f * 6854191149854506640L * -128033296 * 23412341234123414L;
System.out.println("" + a); //K-Java shows 1.8916947877681303e+62, Java shows Infinity

double b = (double) 1 - 1473150328275393513L / 0.16 * 6854191149854506640L * -128033296 * 23412341234123414L;
System.out.println("" + b); //K-Java and Java shows 1.8916947877681303e+62

Additionally, I noticed that K-Java wrongly represents the infinity value (e.g. -Infinity.0) of double or float calculations and also the exponent representation is a bit different to Java.

rschumi0 avatar Feb 29 '20 23:02 rschumi0