--- layout: fc_discuss_archives title: Message 27 from Frama-C-discuss on March 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] [Jessie] Issue with behavior in contracts



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