Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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.