在 frama-c 中添加缺失函数的代码
Adding Code of missing functions in frama-c
原谅我的无知。我需要为一个项目计算反向切片。经过一番搜索，我遇到了 frama-c。我在我的 ubuntu 系统上下载了这个包，它让我得到了 Frama-c 版本：Fluorine-20130601。我是第一次尝试使用它。当在我的项目中发现未定义的函数时，几乎所有的库函数都是未定义的，甚至是 printf、scanf 等（既没有代码也没有函数 printf 的规范）。根据教程，我必须为所有未定义的函数添加存根。我真的必须为我正在使用的每个库函数添加代码，甚至是 printf 吗？请指导。
您应该更新到 Frama-C Phosphorus，它带来了大量关于 Variadic 函数的改进。特别是，当在常量格式字符串上调用函数时，会自动为 printf/scanf-like 生成规范。对于非可变函数，目录 $FRAMA_C_INSTALL/share/libc/*.c 中提供了一些基本实现（在最新版本的 Frama-C 中）。
原谅我的无知。我需要为一个项目计算反向切片。经过一番搜索，我遇到了 frama-c。我在我的 ubuntu 系统上下载了这个包，它让我得到了 Frama-c 版本：Fluorine-20130601。我是第一次尝试使用它。当在我的项目中发现未定义的函数时，几乎所有的库函数都是未定义的，甚至是 printf、scanf 等（既没有代码也没有函数 printf 的规范）。根据教程，我必须为所有未定义的函数添加存根。我真的必须为我正在使用的每个库函数添加代码，甚至是 printf 吗？请指导。
您应该更新到 Frama-C Phosphorus，它带来了大量关于 Variadic 函数的改进。特别是，当在常量格式字符串上调用函数时，会自动为 printf/scanf-like 生成规范。对于非可变函数，目录 $FRAMA_C_INSTALL/share/libc/*.c 中提供了一些基本实现（在最新版本的 Frama-C 中）。