--- layout: fc_discuss_archives title: Message 38 from Frama-C-discuss on May 2011 ---
Hello, it appears that the frama-c-discuss at lists.gforge.inria.fr which should have been the recipient for your e-mail was expanded into a list of e-mail addresses of subscribers. This seems undesirable, and we should probably take steps so that it doesn't happen again. If you did something special to get this result, please explain what you did in a private message to Benjamin.Monate at cea.fr. On Fri, May 27, 2011 at 12:23 PM, krishnateja kesineni <tejakesineni at gmail.com> wrote: > Somehow, we are not able to get the Software to recognize simple errors like > double free . use after free , buffer overflow I should explain that Frama-C's value analysis was designed initially to be useful for the verification of critical, low-level embedded code. It does not focus on giving a meaning to standard functions because these standard functions are not used in this kind of code. Functions malloc() and free() are only supported in an experimental fashion. There are different modelizations of malloc() provided. None is perfect; this is why there are so many of them. For buffer overflows in malloc'ed blocks, you can use the FRAMA_C_MALLOC_INDIVIDUAL modelization: #define FRAMA_C_MALLOC_INDIVIDUAL #include "share/malloc.c" main() { /* out of bounds */ int *p = malloc(3 * sizeof(int)); p[4] = 3; } frama-c -val test_m.c ... test_m.c:9:[kernel] warning: out of bounds write. assert \valid(p+4); In this log message, "assert" indicates a dangerous construct in the source code. The analyzer cannot guarantee that p+4 is valid at this line, and (p+4) SHOULD be valid. In fact, the analyzer is sure that p+4 is not valid, because it says that the executions ends here with this error. The file malloc.c that is included in the test file's first line is the file provided in direction share/ of the soure distribution. This file may have been installed in /usr/share/frama-c for instance if you are using a Linux distribution package. If you compiled yourself on Unix, it is in /usr/local/share/frama-c. Pascal