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?


David MENTRE wrote:
>  2. for read(), the system declaration is "ssize_t read(int fd, void
> *buf, size_t count);". However, the "buf" pointer is to void, that
> Frama-C does not support. For example I cannot declare "requires
> \valid(buf);". And I can't change the declaration to "char *" as it
> would not match the system declaration. Any recommendation? I could
> copy/past the code of read() and redefine it, but I fear I could just
> postpone the issue to another function.

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

notice that \valid((char*)buf) is not enough to prevent buffer overflow

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

- Claude





-- 
Claude March?                          | tel: +33 1 72 92 59 69
INRIA Saclay - ?le-de-France           | mobile: +33 6 33 14 57 93
Parc Orsay Universit?                  | fax: +33 1 74 85 42 29
4, rue Jacques Monod - B?timent N      | http://www.lri.fr/~marche/
F-91893 ORSAY Cedex                    |