防止 Frama-C 的切片插件更改输入代码

Question

给定一个 C 文件，我想根据某些标准计算后向切片并将切片与原始代码进行比较。因为我不想从头开始实现切片程序，所以我已经尝试习惯了 Frama-C，这似乎有助于完成这项任务。

但是，我的问题是，Frama-C 的切片插件更改了预处理的输入代码，因此更难识别原始的哪些行也出现在切片中。

例子：

输入文件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;
}

预处理文件（由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;
}

切片（由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;
}

请注意main 的签名不同，func1 的名称已更改为func1_slice_1。

有没有办法抑制这种行为，以使切片和（预处理的）原始文件更容易比较（就可计算差异而言）？

Answer 1

首先，为了澄清一个您不需要回答但搜索相同关键字的人可以回答的简单问题，您不能将切片程序打印为原始程序的行的选择（两者之间的大部分差异这两者基本上对应于丢失的信息。如果信息在那里，它将被用来打印最相似的程序）。 您可以做的是打印原始程序的 Frama-C 表示，您已经在使用 frama-c test2.c -print -ocode test2_norm.c。

为了解决你func1被重命名为func1_slice_1的问题，你可以试试-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;
}

我认为这将阻止切片器在 func1 内切片。帮助说：

-slicing-level 设置用于传播到 来电 0：不切片调用的函数 1：不切片调用的函数，但传播 反正标记 2：尽量使用已有的切片，最多创建一个 3：最精确的切片