CODEWITHSUNDEEP
frama-c
Philippe Antoine
Philippe Antoine

Reputation: 31

frama-c : how to assume malloc succeeds?

I would like to analyze my program assuming malloc successfully returns an allocated buffer.

When I run the value plugin with the command

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

on this simple program :

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

I get the following output :

[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

I would like not to get the "out of bounds write" How can I do that ?

PS : I tried to change the malloc specification in stdlib.h, without success

Upvotes: 2

Views: 344

Answers (1)

byako
byako

Reputation: 3422

Unfortunately, there is no satisfying implementation of malloc in the current open-source version of Frama-C (in the Value plugin). The previously available versions, in stdlib.c, all had drawbacks. They have been removed partly for this reason.

We have implemented a new, sound (correct) and intelligible enough modelization. However, it will only be available with Frama-C Silicium, to be released in october or november 2016.

Upvotes: 2

Related Questions