frama-c - 在 frama-c 中添加缺失函数的代码

Question

原谅我的无知。我需要为项目计算后向切片。经过一番搜索，我遇到了frama-c。我在我的 ubuntu 系统上下载了这个包，得到了 Frama-c 版本：Fluorine-20130601。我第一次尝试使用它。在我的项目中找出未定义的函数时，几乎所有库函数都是未定义的，甚至 printf、scanf 等（既没有代码也没有函数 printf 的规范）。根据教程，我必须为所有未定义的函数添加存根。我真的必须为我正在使用的每个库函数添加代码，甚至是 printf 吗？请指导。

Answer 1

你应该更新到 Frama-C Phosphorus，它带来了关于 Variadic 函数的大量改进。特别是，当在常量格式字符串上调用类似 printf/scanf 的函数时，会自动生成规范。对于非可变函数，目录中提供了一些基本实现$FRAMA_C_INSTALL/share/libc/*.c（在最新版本的 Frama-C 中）。