c - Frama-C：找到循环结束的位置

问题描述

在以下示例代码中：

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.predslist 并找到了i = 0;and i++。该stmt.succs列表仅包含对的if测试i < ni。
}do 不对应于任何类型的 stmt 或 Instr 并且不存在于stmt.bstmts列表中。
Stmts_graph在like中使用函数get_all_stmt_last_stmts（这给了我一个break语句，并且这个break语句与循环具有相同的位置）不能解决问题。

如何获取循环结束的位置（此处}）。谢谢。

标签： cocamlframa-c

在 Frama-C 中，没有与}代码中的结束相对应的语句之类的东西。仅存在可能具有可观察效果的语句（对内存或控制流）；唯一的例外是Skip，但 Frama-C 避免生成这些。

如果您正在寻找从 AST 中提取的的行号}，您可以查看附加到每个语句的位置的第二个组成部分。从中可以看出Cil_types，位置是成对的Lexing.position，第二个表示指令的结束。然而，Frama-C 很少努力获得该组件的准确信息，因为它从未显示
如果您正在寻找退出循环的 AST 语句，请寻找那些在循环内部，并且其后继（.succs字段）在外部的语句。这个特定的边缘将或多或少与您的}. 在示例的循环中，您应该找到break为处理退出条件而创建的语句。

c - Frama-C：找到循环结束的位置

问题描述

解决方案

推荐阅读