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

[Frama-c-discuss] While/if conditions and slicing



Hello,

I noticed that the slice (output program) produced by Frama-C's Slicing plug-in does not contain the conditions of "if" statements if the plug-in determined that only the statements in one of the branches of the "if" statement affect the value specified by the slicing criterion and not the others (if any). However, the slice always appears to contain the conditions of "while" loops even if the loop body executes only once. To illustrate, here is a small example:

$ cat if.c
int f() {
  int x = 1;
  if (x > 0) {
    x--;
  }
  return x;
}
$ frama-c if.c -main f -slice-return f -then-on 'Slicing export' -print
...
/* Generated by Frama-C */
int f(void)
{
  int x = 1;
  x --;
  return x;
}

As you can see, the slice does not contain the "if" condition. However, if the "if" statement is changed to a "while" loop:

$ cat while.c
int f() {
  int x = 1;
  while (x > 0) {
    x--;
  }
  return x;
}
$ frama-c while.c -main f -slice-return f -then-on 'Slicing export' -print
...
/* Generated by Frama-C */
int f(void)
{
  int x = 1;
  while (x > 0) x --;
  return x;
}

...the slice does contain the condition of the "while" loop. In general, why does the plug-in produce slices that contain "while" conditions but not "if" conditions?

Thanks,
Gilbert