--- layout: fc_discuss_archives title: Message 21 from Frama-C-discuss on March 2009 ---
David MENTRE wrote: > Hello, > > On Tue, Mar 3, 2009 at 17:30, David MENTRE <dmentre at linux-france.org> wrote: >> I would like to define the behaviour of read() syscall. I'm using the >> following contract: >> /*@ requires fd >= 0; >> requires count > 0; >> requires \valid((char*)buf+(0..count-1)); >> behavior error: >> assigns global_error_number; >> ensures \result < 0; >> behavior end_of_file: >> assigns \nothing; >> ensures \result == 0; >> behavior normal: >> assigns ((char*)buf)[0..count-1]; >> ensures ((char*)buf)[0] >= 0 && ((char*)buf)[0] < 256; >> ensures \result > 0; >> */ Even worse: since you have no assumes clauses in your behaviors, then your specification says that at return, the \result is both < 0, == 0 and >0. This is clearly wrong -- 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 |