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_graphlike中的函数get_all_stmt_last_stmts(它给我一个break语句,并且此break语句与循环具有相同的位置)不能解决问题.

如何获得循环结束的位置(此处}).谢谢.

Answer 1

在Frama-C中,没有与}代码中的结束相对应的语句.只存在可能具有可观察效果的语句(在内存或控制流上); 唯一的例外是Skip,但Frama-C避免产生这些.

• 如果你正在寻找的行号的},从AST提取,你可以看一下附加到每个语句的位置的第二部分.可以看出Cil_types,位置是成对的Lexing.position,第二个表示指令的结束.但是,Frama-C不会为此组件提供准确的信息,因为它从未显示过

• 如果您正在寻找退出循环的AST语句,请查找循环内部的那些语句,以及其后继语句(.succs字段)在外部.这个特殊的边缘或多或少会对应你的}.在示例的循环中,您应该找到break为处理退出条件而创建的语句.