--- layout: fc_discuss_archives title: Message 15 from Frama-C-discuss on March 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Best approach when specifying regular C functions from stdlib?



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.