Conditioned Slicing in Frama-C

Question

My last question (Understanding Frama-C slicer results) was on a precise example, but as I said, my goal is to know if it is possible to do some conditioned slicing (forward and backward) with Frama-C. Is it possible?

More precisely, I can't obtain a precise slice of this program :

/*@ requires a >= b;

  @ assigns \nothing;

  @ ensures \result == a;
*/
int example4_instr1(int a, int b){
    int max = a;
    if(a < b)
        max = b;
    return max;
}

Is it possible, by using good parameters/options, to get what I want in this case/in the general case?

Answer 1

As Pascal mentioned in his answer to your previous question, Frama-C's backward and forward slicing are based on the results of an analysis called Value Analysis. This analysis is non-relational; this means that it only keeps information about the numeric range of variables, but not about e.g. the difference between two variables. Thus, it is not able to keep track of your inequality a >= b. This explains why both branches of the test if (a < b) appear to be followed.

Without more information from either the user (but, in this example, nothing that you could write will help the Value Analysis), or another analysis, the backward slicing must consider that the if may or may not be taken. This unfortunately results in a program from which nothing has been sliced away.