--- layout: fc_discuss_archives title: Message 13 from Frama-C-discuss on March 2009 ---
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 |