--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on June 2018 ---
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