--- layout: fc_discuss_archives title: Message 4 from Frama-C-discuss on June 2018 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] beginner question about code using malloc



* 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