4

我正在尝试在特定位置对数组元素执行反向切片。我尝试了两种不同的源代码。第一个是（first.c）：

const int in_array[5][5]={
                          1,2,3,4,5,
                          6,7,8,9,10,
                          11,12,13,14,15,
                          16,17,18,19,20,
                          21,22,23,24,25
};

int out_array[5][5];
int main(unsigned int x, unsigned int y)
{
  int res;
  int i;
  int j;
  for(i=0; i<5; i++){
    for(j=0; j<5; j++){
      out_array[i][j]=i*j*in_array[i][j];
    }
  }
  res = out_array[x][y];
  return res;
}

我运行命令：

frama-c-gui -slevel 10 -val -slice-return 主文件.c

并获得以下生成的代码：

int main(unsigned int x, unsigned int y)
{
  int res;
  int i;
  int j;
  i = 0;
  while (i < 5) {
    j = 0;
    while (j < 5){
      out_array[i][j] = (i * j) * in_array[i][i];
      j ++;
    }
    i ++;
  }
  res = out_array[x][y];
  return res;
}

这似乎没问题，因为 x 和 y 没有定义，所以“res”可以在 out_array 中的任何位置。然后我尝试使用以下代码：

const int in_array[5][5]={
                          1,2,3,4,5,
                          6,7,8,9,10,
                          11,12,13,14,15,
                          16,17,18,19,20,
                          21,22,23,24,25
};

int out_array[5][5];
int main(void)
{
  int res;
  int i;
  int j;
  for(i=0; i<5; i++){
    for(j=0; j<5; j++){
      out_array[i][j]=i*j*in_array[i][j];
    }
  }
  res = out_array[3][3];
  return res;
}

给出的结果完全相同。但是，由于我明确地在数组中寻找特定位置，并且循环是独立的（可并行化的），我希望输出是这样的：

int main(void)
{
  int res;
  int i;
  int j;
  i = 3;
  j = 3;
  out_array[i][j]=(i * j) * in_array[i][j];
  res = out_array[3][3];
}

我不确定这些例子是否清楚。我想要做的是确定，对于给定的数组位置，哪些语句会影响其最终结果。提前感谢您的任何支持。

4

1 回答 1

2

您获得“影响最终结果的陈述”。问题是并非所有循环迭代都是有用的，但是切片无法以当前形式删除代码中的语句。如果您使用 执行句法循环展开，-ulevel 5那么您将个性化每个循环迭代，并且切片可以为每个循环决定是否将其包含在切片中。最后，frama-c-gui -ulevel 5 -slice-return main loop.c给你以下代码

int main(void)
{
  int res;
  int i;
  int j;
  i = 0;
  i ++;
  i ++;
  i ++;
  j = 0;
  j ++;
  j ++;
  j ++;
  out_array[i][j] = (i * j) * in_array[i][j];
  res = out_array[3][3];
  return res;
}

这确实是计算 的值所需的最小指令集out_array[3][3]。

当然，是否-ulevel n扩展到非常高的值n是另一个问题。

于 2015-02-18T17:17:08.747 回答