--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on June 2018 ---
* 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; > } I take the question back. If I guard against malloc returning NULL, EVA is indeed able to see the write being in-bounces! :-) The malloc implementation I use does never return NULL (embedded code). So I can just use a custom malloc spec, where I remove the "or NULL" case. Sorry for the noise. :-) Holger