--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on June 2018 ---
Dear all, someone kindly pointed out to me, that my question got relayed to stackoverflow. Since the answer there was quite helpful and detailed, I thought I might post it here, too. Yes, I do think mailing lists are a great medium. :-) * Holger Kiskowski <holger.ki at freenet.de> wrote: > 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; > } --cut-- The issue is that by default, in Eva, malloc can fail. To avoid this, choose one of the following: 1. use option -no-val-alloc-returns-null, which supposes that malloc never fails; 2. patch the code to add a test, e.g. if (!p) exit(1); The fact that there are 2 possible executions after the malloc is not immediately visible in the command-line. The GUI sometimes helps when inspecting such cases, but we can also add a call to Frama_C_show_each(p) after the call to malloc: char *p = malloc(2); Frama_C_show_each_p(p); ... Now, after running frama-c -val, we get the following line: [value] mall.c:6: Frama_C_show_each_p: {{ NULL ; &__malloc_main_l5 }} The two different possibilities (malloc failed and returned NULL; or malloc succeeded and returned a new base) are considered by the analysis. The alarm Warning: out of bounds write. assert \valid(p + 0); refers to the first case, in which the property is invalid. The analysis stops for this branch, which makes it harder to see what happened, since afterwards we have a single branch, just as we had expected. --cut-- Thanks alot for the replies (on and off-list)! Holger