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

Question

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

对于以前的版本(氮气)，可以通过定义一些符号来选择特定的堆模型，例如:

#define FRAMA_C_MALLOC_HEAP

等等。

Frama-C Neon user manual建议包含文件 share/malloc.c，但我找不到它。

• Frama-C Nitrogen 包含 share/malloc.c 和 share/libc/stdlib.c(包括后者运行良好)；
• Frama-C Fluorine 3 仅包含 share/stdlib.c；
• Frama-C Fluorine 2 均不含 ;
• Frama-C Neon 两者都不包含；

此外 Fluorine 3 changelog列出“添加缺少的 C 库文件。”

FRAMA_C_MALLOC_* 符号是否已弃用或 Neon 源代码分发是否有些不完整？

Answer 1

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