Real arithmetic is used even on integer values (Numerical analysis of Java programs)

[maemre]

It seems like Jandom uses real arithmetic rather than integer arithmetic when abstracting integer arithmetic operations. When I run numerical analysis (using BoxDouble domain) on Jimple code of JimpleTest.idiv() from Java examples, I get the following output:

    static void idiv()
    {
        byte b0, b1;
        int i2;

/*[ [ -∞ ≤ b0 ≤ +∞ , -∞ ≤ b1 ≤ +∞ , -∞ ≤ i2 ≤ +∞ ]types: byte,byte,int ]*/
        b0 = 15;

/*[ [ b0 = 15.0 , -∞ ≤ b1 ≤ +∞ , -∞ ≤ i2 ≤ +∞ ]types: byte,byte,int ]*/
        b1 = 2;

/*[ [ b0 = 15.0 , b1 = 2.0 , -∞ ≤ i2 ≤ +∞ ]types: byte,byte,int ]*/
        i2 = b0 / b1;

/*[ [ b0 = 15.0 , b1 = 2.0 , i2 = 7.5 ]types: byte,byte,int ]*/
        return;
    }
/* Output: [ b0 = 15.0 , b1 = 2.0 , i2 = 7.5 ]types: byte,byte,int */

Notice that the analysis concludes that i2 = 7.5 at the end but i2 = 7 if you run the program because of integer division.

BoxDouble over reals and Parallelotope over rationals have different manifestations of the same issue as well.

[amato-gianluca]

You are right, there is a problem there. I will try to fix it as soon as I come back to work (a couple of weeks).