Value Dependency Analysis with Frama-C

Question

At the end of the following program, the value of variable x depends on the set of variables {x,y,z,c}. Similarly, the value of variable y depends on the set of variables {y,c}.

int main(){
    int x = 100;
    int y = 50;
    int z = 20;
    int c = g();

    if (c){
        x += y + 1;
    }else{
        x += z + 1;
        y = y + 1;
    }

    return 0;
}

Can I get this information from the Frama-c tool from the command line? If yes, I would highly appreciate if someone could help me with this.

Answer 1

You cannot obtain this result from one of the existing plugins of Frama-C on the main function you supplied. But, if you modify your code a bit, the plugin From will return exactly the information you want.

// test.c
int x = 100;
int y = 50;
int z = 20;

extern int c; // unknown value

int main(){

    if (c){
        x += y + 1;
    }else{
        x += z + 1;
        y = y + 1;
    }

    return 0;
}

frama-c -deps test.c

[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
       These dependencies hold at termination for the executions that terminate:
[from] Function main:
  x FROM x; y; z; c
  y FROM y; c (and SELF)
  \result FROM \nothing
[from] ====== END OF DEPENDENCIES ======

The results for x are self-explaining. For y, you get the additional information that y may be unchanged since the beginning of the function, hence the (and SELF).

The reason you get different results by initializing the variables out of main is due to the fact that the -deps analysis computes its results w.r.t. the state at the beginning of the function. In your main, since x, y and z are set to constant values, their final results depend only on c, which in turns only depends on what g reads to compute its result.