--- layout: fc_discuss_archives title: Message 13 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?




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                    |