--- layout: fc_discuss_archives title: Message 15 from Frama-C-discuss on March 2009 ---
On Tue, Mar 3, 2009 at 15:15, Claude March? <Claude.Marche at inria.fr> wrote: > I suggest > > /*@ requires \valid((char*)buf+(0..count-1)); > ? @ ... > > this is quite consistent with the informal spec of read, where count > denote the number of *bytes* to read Ok. Thank you. > notice that \valid((char*)buf) is not enough to prevent buffer overflow Yes. It was a first attempt when trying to understand this void* issue. > Finally, I said before that Frama-C is not shipped with spec for > standard lib functions, but this is not completely true: there are > specifications for strings functions, in jessie_prolog.h file. You > should have a look at them Ok. While playing with print of pre-processed file I have seen it. I'll look at it. Many thanks, Yours, d.