--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on March 2010 ---
Hello, > I have a problem running the slicing tool. I am using the following options > > frama-c -slice-print -slice-wr Variable -slice-rd Variable file.c > > The Variable is a global but the slicer, slices everything up to a > certain point even though assignments to Variable exist further down the > execution path. I am running frama-c Beryllium-20090902. Could anyone > explain what might be happening? One possibility, which is only a special case of the situation Anne described, is that Frama-C thinks that a run-time error is certainly happening. Consider the example: int Variable ; int x; int main(){ Variable = 1; x = 100; Variable = 2; x = 100 / Variable; Variable = 0; x = 200 / Variable; Variable = 5; return Variable; } With your commandline, this is sliced into: int Variable ; int x ; void main(void) { Variable = 1; Variable = 2; x = 100 / Variable; Variable = 0; /*@ assert (Variable ? 0); // synthesized */ x = 200 / Variable; return; } Frama-C considers you are not interested in the assignment Variable=5; because it happens after a guaranteed division by zero. Indeed, it wouldn't be executed in a real execution of the original program, so it doesn't have to be in the sliced program. Pascal