--- layout: fc_discuss_archives title: Message 9 from Frama-C-discuss on March 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] question about slicer



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