--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on June 2018 ---
Dear all, hopefully this is not too much of a FAQ. I first thought it would be, but I found surprisingly few sample code using malloc (that I was able to get to run). How can I verify this C program using frama-c? #include <stdlib.h> int main(void) { char *p = malloc(2); char s[2]; p[0] = 0; s[0] = 0; return 0; } When I run the yesterday released version on this code, I get $ frama-c -val t.c [kernel] Parsing t.c (with preprocessing) [value] Analyzing a complete application starting at main [value] Computing initial state [value] Initial state computed [value:initial-state] Values of globals at initialization __fc_heap_status â [--..--] __fc_random_counter â [--..--] __fc_rand_max â {32767} __fc_mblen_state â [--..--] __fc_mbtowc_state â [--..--] __fc_wctomb_state â [--..--] [value] t.c:5: allocating variable __malloc_main_l5 [value:alarm] t.c:7: Warning: out of bounds write. assert \valid(p + 0); [value] done for function main [value] ====== VALUES COMPUTED ====== [value:final-states] Values at end of function main: __fc_heap_status â [--..--] p â {{ &__malloc_main_l5[0] }} s[0] â {0} [1] â UNINITIALIZED __retres â {0} __malloc_main_l5[0] â {0} [1] â UNINITIALIZED Apparently the value plugin knows about the size of the allocated chunk with malloc. And it correctly infers the write to s[0] as valid. (tested by writing to s[3]! :-)) But who could I tell it to discharge the \valid(p+0) goal? I also tried the wp plugin, but it says that allocation is not supported yet. Thanks alot, Holger