search

goblint / analyzer

Static analysis framework for C
https://goblint.in.tum.de
MIT License
184 stars 75 forks source link

Fixpoint not reached for Poly analysis #168

Closed ivanazuzic closed 3 years ago

ivanazuzic commented 3 years ago

The current implementation of Poly analysis (uses polyhedra from Apron) doesn't reach the fixpoint for the following example:

// PARAM: --set ana.activated[+] "'poly'" --enable dbg.debug --enable ana.int.interval

int main(void) {
    int x, y, r;
    x = 5;
    y = 3;
    r = x + y; 
    while (x != y) {
        assert(r > 0); 
        if (y > x) 
            y = y - x;
        else 
            x = x - y; 
        assert(r > x + y); 
        r = x + y;
    }
    return 0;
}
sim642 commented 3 years ago

The current octApron (to be renamed to apron in #335) even when switching from Oct.t to Polka.loose Polka.t (to use polyhedra for things like r = x + y) cannot prove the asserts, but at least reaches a fixpoint. I guess whatever the original issue was, got fixed at some point. If these asserts should go through with polyhedra, I guess one has to investigate again, why they currently wouldn't.