frama-c - 切片程序中未声明的变量

Question

在使用 Frama-C 版 Oxygen 的程序切片器时，我遇到的问题是生成的切片使用了未声明的变量。我之前搜索过该主题的现有帖子，发现： http ://bts.frama-c.com/print_bug_page.php?bug_id=806

那里提到该错误已在 Frama-C 的 Nitrogen 版本中修复。也许这种变化并没有转移到氧气上？就像在现有帖子的描述中一样，它只发生在只有一个语句的块中。我无法附上示例源代码，因为它来自客户项目。

Answer 1

我已经检查了您使用 Frama-C Oxygen 提到的错误报告中描述的确切步骤（以及用于 Csmith 运行时库的 csmith 2.0.0），并且一切正常：您很可能遇到了另一个问题，但没有代码，不能多说。