帧-c : how to assume malloc succeeds?

Question

我想分析我的程序，假设 malloc 成功返回分配的缓冲区。

当我使用命令运行值插件时

/Users/philippeantoine/.opam/4.02.3/bin/frama-c -val testalloc.c

在这个简单的程序上:

#include <stdlib.h>
int main (){
    char * test = malloc(10);
    test[0] = 'a';
}

我得到以下输出:

[value] computing for function malloc <- main.
    Called from testalloc.c:4.
[value] using specification for function malloc
[value] Done for function malloc
testalloc.c:5:[kernel] warning: out of bounds write. assert \valid(test+0);
[value] Recording results for main
[value] done for function main

我不想得到“越界写入” 我怎样才能做到这一点？

PS:我尝试更改 stdlib.h 中的 malloc 规范，但没有成功

Answer 1

不幸的是，在当前的 Frama-C 开源版本(在 Value 插件中)中没有令人满意的 malloc 实现。 stdlib.c 中以前可用的版本都有缺点。由于这个原因，它们已被部分删除。

我们已经实现了一种新的、合理的(正确的)且足够易懂的模型化。不过，它只能与 Frama-C Silicium 一起使用，将于 2016 年 10 月或 11 月发布。