我已经成功编译了 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 源代码分发是否有些不完整?
最佳答案
是的,一些与建模动态内存分配相关的文件已从 Neon Frama-C 版本中删除。
关于c - Frama-C Neon 缺少 C 库文件?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/23249448/