Loading Octagons breaks floating point addition

[svenkeidel]

Hi, I found another obscure bug in the Java bindings.

public class OctagonTest {
    public static void main(String args[]) {
        double x = -1E308d;
        double y = -1E308d;
        System.out.printf("%e + %e = %e\n",  x, y, x + y); // Outputs -1.000000e+308 + -1.000000e+308 = -Infinity
        new apron.Octagon();
        System.out.printf("%e + %e = %e\n", x, y, x + y);  // Outputs -1.000000e+308 + -1.000000e+308 = -1.797693e+308
    }
}

I have absolutely no idea what is going on here. My best guess would be that the loading of the native library in line new apron.Octagon() corrupts the memory somehow. But I don't understand how this would break floating point addition.

Furthermore, this doesn't happen with Polka, so it seems to be an octagon issue.

@antoinemine, does this happen in OCaml/C as well?

[antoinemine]

This behavior is expected. Floating-point domains, such as octagons, have to put the FPU in rounding towards +oo mode to be sound. This occurs when the octagon class is loaded, hence between the two prints. In this mode, a very large (in absolute value) negative number is rounded to min-float, not minus infinity.

[svenkeidel]

Makes sense. Thanks.