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