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)?

score 2 · Answer 1 · answered Mar 04 '16 at 10:56

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

OK, That almost does the job. However, you;re right, it will prevent the slicer from slicing func1 at all, which is not what I want actually :-/ I gues there is no obvious way to only prevent it from renaming the function so I might probably have to tamper with Frama-C' source code — Paddre, Mar 04 '16 at 15:11
@Paddre Yes, all options except 3 should create at most one new version of `func1` so you could hope to keep it named `func1`. The devil is in the details though. Try your luck in a file named `slicingMacros.ml`, or perhaps you could just use a regexp (possibly changing `slicingMacros.ml` only to make it even more amenable to regexp substitution) to change all occurrences of X_slice_1into X? — Pascal Cuoq, Mar 04 '16 at 16:11
Actually it was not `slicingMacros.ml` I had to edit, but `slicingTransform.ml` (editing the appropriate line in `slicingMacros.ml` does not seem to have any effect). I'll edit your answer so that I can mark it as "Accepted" — Paddre, Mar 08 '16 at 12:31
Oh right, I grepped for `"_slice` and found only the former, but now that you mention it I see that `slicingTransform.ml` contains expressions like `Printf.sprintf "%s_slice_%d" fname ff_num` that would be good places to tweak too. Glad you (apparently) managed to get it working. — Pascal Cuoq, Mar 08 '16 at 14:46

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

1 Answers1