Prevent Frama-C's slicing plugin from changing input code

Question

Given a C file, I want to compute the backward slice for some criteria and compare the slice to the original code. Because I don't want to implement a slicing program from cratch, I've already tried to get used to Frama-C which seems to help with this task.

However, my problem is, that Frama-C's slicing plugin changes the preprocessed input code, so that it makes it harder to identify which lines of the original also appear in the slice.

Example:

Input file test1.c:

double func1(double param) {
    return 2+param;
}

int main() {
    int a=3;
    double c=4.0;
    double d=10.0;
    if(a<c)
        c=(double)a/4.0;
    double res = func1(c);
    return 0;
}

Preprocessed file (yielded by frama-c test1.c -print -ocode test1_norm.c):

/* Generated by Frama-C */
double func1(double param)
{
  double __retres;
  __retres = (double)2 + param;
  return __retres;
}

int main(void)
{
  int __retres;
  int a;
  double c;
  double d;
  double res;
  a = 3;
  c = 4.0;
  d = 10.0;
  if ((double)a < c) c = (double)a / 4.0;
  res = func1(c);
  __retres = 0;
  return __retres;
}

Slice (yielded by frama-c -slice-calls func1 test1.c -then-on 'Slicing export' -print):

/* Generated by Frama-C */
double func1_slice_1(double param)
{
  double __retres;
  __retres = (double)2 + param;
  return __retres;
}

void main(void)
{
  int a;
  double c;
  double res;
  a = 3;
  c = 4.0;
  c = (double)a / 4.0;
  res = func1_slice_1(c);
  return;
}

Note that the signature of main differs and that the name of func1 was changed to func1_slice_1.

Is there a way to suppress that behaviour in order to make the slice and the (preprocessed) original more easily comparable (in terms of a computable diff)?

Answer 1

First, to clarify a simpler question that you don't need answering but that someone searching for the same keywords could, you cannot have the sliced program printed as a selection of the lines of the original program (most of the differences between the two corresponds to lost information, basically. If the information was there, it would be used to print the most resembling program possible). What you can do is print Frama-C's representation of the original program, which you are already doing with frama-c test2.c -print -ocode test2_norm.c.

To solve your problem of func1 being renamed to func1_slice_1, you can try playing with option -slicing-level 0:

$ frama-c -slicing-level 0 -slice-calls func1 test1.c -then-on 'Slicing export' -print
...
/* Generated by Frama-C */
double func1(double param)
{
  double __retres;
  __retres = (double)2 + param;
  return __retres;
}

void main(void)
{
  int a;
  double c;
  double res;
  a = 3;
  c = 4.0;
  c = (double)a / 4.0;
  res = func1(c);
  return;
}

I think this will prevent the slicer from slicing inside func1 at all. The help says:

-slicing-level <n>  set the default level of slicing used to propagate to the
                    calls
                    0 : don't slice the called functions
                    1 : don't slice the called functions but propagate the
                    marks anyway
                    2 : try to use existing slices, create at most one
                    3 : most precise slices