Frama-C 内置值

Question

我刚刚从 Opam 包管理器中安装，并且正在尝试从 frama-c 网站上的教程中学习如何使用价值分析。我目前无法使用 builtin.c 文件，它不在我的共享文件夹中，我无法弄清楚如何使用 -val-builtin （如果这甚至合适的话）。

关于如何实现这一点的任何想法？

我安装了 Frama-c 的 20151002 版本。

感谢您的帮助！

Answer 1

诸如 Frama_C_interval 之类的 Frama-C “半内置”不再需要由 Value 分析的实现。因此，大部分builtin.c 已被删除，其余部分已内联到其他文件中。手册中提到的所有builtin.c 都可以忽略，前提是包含__fc_builtin.h。同样，builtin.h 已替换为 __fc_builtin.h。 （但会发出警告以提醒用户注意这一事实。）我们将更新 Frama-C 铝的手册以澄清这一点。

关于应该使用哪个版本，我强烈建议您使用 Magnesium (20151002)。这些年来已经有了很多改进。