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.