java-semantics
java-semantics copied to clipboard
wrong precision for floats
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.