Срез Frama-C: распараллеливаемая петля

Question

Я пытаюсь выполнить обратную нарезку элемента массива в определенной позиции. Я попробовал два разных исходных кода. Первый (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];
}

Я не уверен, ясно ли это из примеров. Что я хочу сделать, это определить для данной позиции массива, какие операторы влияют на его конечный результат. Заранее спасибо за любую поддержку.

Answer 1

Вы получаете "утверждения, которые влияют на конечный результат". Проблема заключается в том, что не все итерации цикла полезны, но у среза нет способа удалить оператор в коде в его текущей форме. Если вы выполните развертывание синтаксического цикла, с -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 это другой вопрос.