pascal-lab / Tai-e-assignments

Tai-e assignments for static program analysis
https://tai-e.pascal-lab.net/
GNU Lesser General Public License v3.0
1.01k stars 234 forks source link

improvement of assignment2 #11

Open Z3ratu1 opened 1 year ago

Z3ratu1 commented 1 year ago

I think when some value*0, the result should be 0, same for 0/some value and 0 % some value, but OJ judged me wrong in testcase Switch.java

class Switch{
    int switch1(int x, int y){
        int a = 0;
        switch(x){
            case 1:
                a-=y;
                break;
            case 2:
                a+=y;
                break;
            case 3:
                a*=y;
                break;
            case 4:
                a/=y;
                break;
            default:
                a = a-1;
        }
        a = a+x;
        return a;
    }

in case3/4 a must be zero, but the answer is NAC

------ Failure on <Switch: int switch1(int,int)> ------
Expected: [9@L12] a = a * y; {a=NAC, x=NAC, y=NAC}
Expected: [10@L13] goto 21; {a=NAC, x=NAC, y=NAC}
epitaphial commented 9 months ago

I guess maybe it only considers the general and abstract value in the lattice, rather than the concrete case...