3

给定一个 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。

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

4

1 回答 1

2

首先，为了澄清一个您不需要回答但搜索相同关键字的人可以回答的简单问题，您不能将切片程序打印为原始程序行的选择（两者之间的大部分差异对应基本上是为了丢失信息。如果信息在那里，它将被用来打印最相似的程序）。您可以做的是打印 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 <n> 设置用于传播到
                    来电
                    0：不切片调用的函数
                    1：不切片调用的函数，但传播
                    反正标记
                    2：尽量使用已有的切片，最多创建一个
                    3：最精确的切片
于 2016-03-04T10:56:44.063 回答