The frama-c impact analysis can't analysis control dependence?

Question

When I use the frama-c analysis my c program. It seems there exits a bug in the impact plug in of the frama-c. This is my program.

#include<stdio.h>
int global;
int main()
{
    global = 12;
    int result = 0;
    if(global > 1)
    {
         result += 100;
    }
    else
    {
        result += 200;
    }
    return 0;
}

I want to find all the stataments impacted by the variable "global". Obviously, the statement "result += 100;" in the scope of "if condition" which is related to the variable "global", so the statement "result += 100;" should be high light. However, the running result seems not correct.

Answer 1

I'm assuming that you have used no special option, and that you have started the impact analysis in Frama-C's GUI, on the statement global = 12. If it is not the case, please provide more detailed instructions.

In your program, the if (global > 1) instruction gets selected because there is a data dependency to the statement global = 12. However, the statement result += 100 does not get selected by the Impact plugin. This is the intended behavior, because there is no control dependency in this case. Notice that the else branch of the if is dead. Thus, the execution of result += 100 does not really depend on the evaluation of if (global > 1), as the condition is always true. As the control flow always reaches result += 100 instruction, no control dependency exists.

If you want to exhibit a control dependency in this example, the simplest way consists in changing your line global = 12 into

global = Frama_C_interval(0,100);

and to add the file $(SHARE)/frama-C/libc/__fc_builtin.c to the command-line. The two instructions result += 100 and result += 200 will get selected, in each case because of a control dependency.