原谅我的无知。我需要为项目计算向后切片。搜索后，我遇到了Frama-C。我在Ubuntu系统上下载了包裹，该软件包使我获得了Frama-C版本：Fluorine-20130601。我试图第一次使用它。当找出我项目中的未定义功能时，几乎所有库功能都是未定义的，甚至是printf，scanf等(函数printf的代码也不是规范(。根据教程，我必须为所有未定义功能添加存根。我是否真的必须为我使用的每个库函数添加代码？请指导。
您应该更新到frama-c磷，这为变异功能带来了很多改进。特别是，当调用恒定格式字符串时，将对printf/scanf样函数自动生成规格。对于非variadic函数，目录$FRAMA_C_INSTALL/share/libc/*.c中有一些基本实现(在Frama-C的最新版本中(。