我发现如果程序中有一个未初始化的左值（例如变量 X），Frama-C 断言 X 已被初始化，但随后断言最终状态无效。似乎 Frama-C 在检测到无效的最终状态后停止了分析，因此影响分析的实际结果（受影响的语句）只是理想结果的一部分。无论那些未初始化的变量如何，我都希望 Frama-C 继续进行影响分析，但我还没有找到任何相关选项。如何处理这个问题？
问问题
80 次
1 回答
2
您正在调用 ISO C 标准附件 J.2 中所示的未定义行为“具有自动存储持续时间的对象的值在不确定时被使用”（语言律师注意：所述附件提供信息，我已经无法将该声明追溯到标准的规范部分，至少对于 C11）。Impact analysis 内部使用的 EVA 插件将其自身限制为根据标准具有明确定义的执行路径（众所周知的鼻恶魔不是 EVA 抽象域的一部分）。如果没有这样的路径，抽象执行确实会停止。处理这个问题的适当方法是确保被分析程序的局部变量在被访问之前被正确初始化。
更新
我忘了在下一个版本（16 - Sulfur）中提及，其测试版可在https://github.com/Frama-C/Frama-C-snapshot/wiki/downloads/frama-c-Sulfur-20171101获得-beta.tar.gz，EVA 有一个 option -val-initialized-locals，其帮助指定：
局部变量进入完全初始化的范围。仅对分析程序错误 wrt 初始化有用。
于 2017-11-13T08:00:02.747 回答