Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] While/if conditions and slicing
  • From: gpajela at GradCenter.cuny.edu (Gilbert Pajela)
  • Date: Thu, 12 Mar 2020 23:04:32 +0000
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