frama-c - 镁中 -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.

我怀疑这两个注释之间存在不匹配，因为它们都具有相同的“名称”: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 后，然后单击“值分析”面板中的“运行”按钮, 我得到了绿色子弹。

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

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

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

技术细节:Frama-C 具有属性 和状态 的概念，源代码旁边的项目符号对其进行了总结，但是通过属性面板(您可能需要修改一些过滤器并单击刷新按钮以查看它们)或报告插件(例如 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 的消息面板中。这并不能解释错误，但是消息和属性面板的组合是诊断属性问题的强大工具。