--- layout: fc_discuss_archives title: Message 5 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



Le 03/06/2018 à 19:46, Holger Kiskowski a écrit :
> 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.


You could also try the `-no-val-alloc-returns-null` options, I guess.

Best,

-- 
François Bobot