Frama-C: найти местоположение конца цикла

Question

В следующем примере кода:

void kernel(int ni, int nj, int nk, float alpha, float *tmp, float *A, float *B) {
int i, j, k;
  for (i = 0; i < ni; i++) {
    for (j = 0; j < nj; j++) {
      tmp[i * nj + j] = 0.0f;
      for (k = 0; k < nk; ++k) {
        tmp[i * nj + j] += alpha * A[i * nk + k] * B[k * nj + j];
      }
    }
}
}

Я попытался получить местоположение } (которое отмечает конец каждого цикла), но безуспешно.

• Например, для первого цикла я просмотрел список stmt.preds и нашел только i = 0; и i++. Список stmt.succs содержит только тест if для i < ni.
• } не соответствует ни одному из типов stmt или Instr и не существует в списке stmt.bstmts.
• Использование функций в Stmts_graph, таких как get_all_stmt_last_stmts (которые дают мне оператор break, а этот оператор break находится в том же месте, что и цикл), не решают проблему.

Как узнать местоположение конца моего цикла (здесь }). Спасибо.

Answer 1

В Frama-C нет такого понятия, как оператор, который бы соответствовал закрывающему } в вашем коде. Существуют только операторы, которые могут оказывать наблюдаемое влияние (либо на память, либо на поток управления); единственное исключение - Skip, но Frama-C избегает их генерации.

• Если вы ищете номер строки из }, извлеченный из AST, вы можете посмотреть на второй компонент местоположений, которые прикреплены к каждому выражению. Как видно из Cil_types, местоположения - это пары Lexing.position, а вторая представляет конец инструкции. Однако Frama-C прилагает незначительные усилия для получения точной информации для этого компонента, поскольку она никогда не отображается

• если вы ищете операторы AST, которые выходят из цикла, ищите те, которые находятся внутри цикла, и чей преемник (поле .succs) находится снаружи. Этот конкретный край будет более или менее соответствовать вашему }. В цикле вашего примера вы должны найти оператор break, созданный для обработки условия выхода.

Answer 2

, чтобы определить, когда циклы запускаются / останавливаются, используют последовательный отступ.

1. отступ после каждой открывающей скобки '{'
2. отступ перед каждой закрывающей скобкой '}'
3. предлагаем, чтобы каждый уровень отступа составлял 4 пробела.

Применение приведенных выше критериев к опубликованному коду приводит к:

void kernel(int ni, int nj, int nk, float alpha, float *tmp, float *A, float *B)
{
    int i, j, k;

    for (i = 0; i < ni; i++)
    {
        for (j = 0; j < nj; j++)
        {
            tmp[i * nj + j] = 0.0f;

            for (k = 0; k < nk; ++k)
            {
                tmp[i * nj + j] += alpha * A[i * nk + k] * B[k * nj + j];
            }
        }
    }
}

, что очень легко увидеть, где начинается и заканчивается каждый цикл