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

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

Answer 1

确定循环何时 start/stop 使用一致的缩进。

在每个左大括号'{'后缩进
在每个右大括号 '}' 之前取消缩进
建议每个缩进级别为 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];
            }
        }
    }
}

这很容易看出每个循环的开始和停止位置

Answer 2

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

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

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

Frama-C: find location of loop end

c

ocaml

frama-c