镁中 -rte 选项的不正常行为

Question

我在 Magnesium 版本（直接从 ubuntu 安装）中遇到 -rte 选项的不连贯行为。我想知道是否有人知道这个问题或者我做错了什么。

我有一个程序在数组外访问不正确。在没有选项和值分析的情况下启动 frama-c-gui 时，会检测到越界访问，并以橙色圆圈显示相应的注释。使用 -rte 选项时，会显示两个注释（数组的下限和上限），并且两者都显示一个绿色圆圈（这是不正确的）。

/*@ assert rte: index_bound: 0 ≤ cpt; */
/*@ assert rte: index_bound: cpt < 5; */

控制台显示：

tableau_erreur.c:11:[value] Assertion 'rte,index_bound' got status valid.

我怀疑这两个注释之间存在不匹配，因为它们都具有相同的 "name" : index_bound.

此外，包含错误访问的循环之后的代码部分显示为红色，这表明分析正确地推断出由于之前的错误而无法访问。

这是我的程序：

int main(){
  int t[5] = {1,2,3,4,5};
  int cpt =0 ;
  int tmp ;
  while  (cpt<10){
    tmp = getchar() ;
    if ( t[cpt] > tmp )
      { return 1  ;  }
    cpt++ ;
  }
  return 10 ;
}

这是我的显示截图（使用 frama-c-gui -rte tableau_erreur.c）。

当我不使用 -rte 选项时，结果是正确的（橙色圆圈）：

我查看了错误跟踪器，但没有找到它的踪迹。我没有设法编译更新版本的 Frama-C 来测试它。

Answer 1

更新：此行为已在 Frama-C 的硅版本中得到修复（与断言 rte: index_bound: cpt < 5 相关的状态仍然是未知).

我无法完全重现您所说的内容，但是按照您的命令启动 GUI 后，然后单击 "Run"按钮在价值分析面板，我得到了绿色的子弹。

这相当于运行 frama-c-gui -rte -then -val，它也显示绿色（不正确）项目符号。

事实上，即使在当前的 Frama-C 版本中，这似乎也是一个问题，因此需要提交错误报告。请注意，手动插入等效注释 (//@ assert cpt < 5;) 确实会如预期那样产生黄色项目符号。此外，展开循环（例如使用 -slevel 5）也会产生黄色项目符号。这个问题似乎与RTE插件的使用特别相关，但无论如何都会进行调查。

附带说明一下，属性旁边的 index_bound 标签不是标识符，只是一个标签，因此不是唯一的，与此处的问题无关。

技术细节：Frama-C有属性和状态的概念，它们是由源代码旁边的项目符号总结，但通过 Properties 面板进行了更详细的描述（您可能需要修改一些过滤器并单击 Refresh 按钮来查看它们）或报告插件（例如 frama-c -val -then -report）。在您的示例中，循环的第一次迭代的 cpt 值为 0，因此属性获得 valid 状态（绿色项目符号），并且在最后一次迭代中（当cpt 是 5) 它获得 unknown 状态（黄色项目符号）。由于某种原因，它被（错误地）合并为 valid，因此是绿色项目符号。然而，值日志确实显示 file.c:8:[value] warning: assertion 'rte,index_bound' got status unknown，它显示在 GUI 的消息面板中。这并不能解释错误，但是消息和属性面板的组合是诊断属性问题的强大工具。

镁中 -rte 选项的不正常行为

Unsound behavior with -rte option in Magnesium

frama-c