Search code examples
cframa-cabstract-interpretation

Automatic widening in frama-c value analysis

I am looking for a method to perform widening on loops with no user hints. I'll explain using an example: 

int z;
void main(void) {   
    int r = Frama_C_interval(0, MAX_INT);
    z = 0;
    for (int y=0; y<r; y++)
        z++;
}

When running frama-c value analysis on this code, the global variable z receives the interval [--,--]. Because z was set to zero and the loop consists of an incremental operator, an automatic widening method should be able to deduct that the more accurate interval is [0, --]. Is it possible to do this in Frama-C?

Solution

  • When running frama-c value analysis on this code, the global variable z receives the interval [--,--].

    No it doesn't:

    ~ $ frama-c -version ; echo
Magnesium-20151001+dev
~ $ cat t.c
#define MAX_INT 0x7fffffff

int z;
void main(void) {   
    int r = Frama_C_interval(0, MAX_INT);
    z = 0;
    for (int y=0; y<r; y++)
        z++;
}
~ $ frama-c -val t.c
…
t.c:8:[kernel] warning: signed overflow. assert z+1 ≤ 2147483647;
…
[value] Values at end of function main:
  z ∈ [0..2147483647]
…

    This is a development version, but the same should apply to any version since signed overflow started to be treated as a serious error with ACSL alarm. If you are using a version from when signed overflow was assumed to harmlessly produce 2's complement results, 1) you should upgrade, it has been years and 2) z can hardly be argued to be trivially positive then (although it is positive because of a relational invariant linking the values of z and y while the loop is executing, relational invariant that the value analysis cannot represent).