我在 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 来测试它。
最佳答案
更新 :此行为已在 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 的消息面板中。这并不能解释错误，但消息和属性面板的组合是诊断属性问题的强大工具。
关于frama-c - Magnesium 中 -rte 选项的不良行为，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/40763614/