c - Frama-C Neon 缺少 C 库文件？

Question

我已经成功编译了 Frama-C Neon (Ubuntu) 以及 Why2、Why3 和 Coq。

在以前的版本（Nitrogen）中，可以通过定义一些符号来选择特定的堆模型，例如：

#define FRAMA_C_MALLOC_HEAP

等等。

Frama-C Neon 用户手册建议包含该文件，share/malloc.c但我找不到它。

• Frama-C Nitrogen 包含share/malloc.c和share/libc/stdlib.c（包括后者工作正常）；
• Frama-C 氟 3share/stdlib.c仅包含；
• Frama-C Fluorine 2 均不含；
• Frama-C Neon 两者都不包含；

此外，Fluorine 3 更改日志列出了“添加缺少的 C 库文件”。

符号是否FRAMA_C_MALLOC_*已弃用，或者 Neon 源分布是否有些不完整？

Answer 1

是的，一些与动态内存分配建模相关的文件已从 Neon Frama-C 版本中删除。