--- layout: fc_discuss_archives title: Message 27 from Frama-C-discuss on March 2009 ---
Hello Claude, On Wed, Mar 4, 2009 at 14:54, David MENTRE <dmentre at linux-france.org> wrote: > On Wed, Mar 4, 2009 at 12:46, Claude March? <Claude.Marche at inria.fr> wrote: >> So, to specify read() I suggest : >> >> /*@ requires fd >= 0; >> ? ? requires count > 0; >> ? ? requires \valid((char*)buf+(0..count-1)); >> ? ? assigns global_error_number, ((char*)buf)[0..count-1]; >> ? ? ensures ... (see below) >> ? @*/ After re-reading the man of read(2), I followed your advice and used the much simpler contract: /*@ requires fd >= 0; requires count > 0 && count <= SSIZE_MAX; requires \valid((char*)buf+(0..count-1)); assigns global_error_number; assigns ((char*)buf)[0..count-1]; */ ssize_t read(int fd, void *buf, size_t count); It is astonishing how C stdlib functions are loosely specified. :-) Sincerely yours, david