Frama-C-discuss mailing list archives
This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Frama-c-discuss] [Jessie] Issue with behavior in contracts
- Subject: [Frama-c-discuss] [Jessie] Issue with behavior in contracts
- From: Claude.Marche at inria.fr (Claude Marché)
- Date: Wed, 04 Mar 2009 12:46:41 +0100
- In-reply-to: <3d13dcfc0903030830m26d0d328n1ac6057eed4a1ff8@mail.gmail.com>
- References: <3d13dcfc0903030830m26d0d328n1ac6057eed4a1ff8@mail.gmail.com>
David MENTRE wrote: > Hello, > > 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; > */ > // complete behaviors error, end_of_file, normal; > ssize_t read(int fd, void *buf, size_t count); > > However, when I run frama-c -jessie-analysis, I have the following > error message: > No code for function read, default assigns generated > > Is my contract for read() really taken into account? In that case, is > it a spurious error message? This warning comes from the fact that you did not give a "global" assigns clause, i.e. outside of any behavior. If you add, after the requires clauses : assigns global_error_number, ((char*)buf)[0..count-1]; More importantly, your use of behaviors is unfortunately wrong. When a contract looks like assigns L1,L2; behavior b: assumes A; assigns L1; then it means that, in any case, only locations L1 and L2 can be modified, and if in the pre-state A is true, then only locations L1 can be modified. But since you do not use any assumes clauses, then the contract is not right, in particular the behavior end_of_file specifies that read() do not modifies anything in any case. Generally speaking, your behaviors corresponds to different cases for the \result, in the post-state, but behaviors have been designed for case distinction in the pre-state (this has been extensively discussed in the ACSL design meetings...) 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) @*/ indeed, by looking your behaviors, I don;t even understand what do you want to specify : > behavior error: > assigns global_error_number; > ensures \result < 0 ; do you want to say "if result is < 0 then global_error_number is set" or something ? > behavior end_of_file: > assigns \nothing; > ensures \result == 0; do you want to say if "if result is zero then nothing is modified ?" it would give : \result == 0 ==> global_error_number == \old(global_error_number) && forall integer i; 0 <= i < count ==> buf[i] == \old(buf[i]) (by the way, is it true that read() does not modify errno in case of success ? is it guaranteed ?) > behavior normal: > assigns ((char*)buf)[0..count-1]; > ensures ((char*)buf)[0] >= 0 && ((char*)buf)[0] < 256; > ensures \result > 0; it seems to me that specifying that a given char is between 0 and 255 is useless (well, if these are *unsigned* char...) May be you should just start without ensures clauses at the beginning, and then try to guess what property you would need after a call to read to prove your program - Claude - 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 |
- Follow-Ups:
- [Frama-c-discuss] [Jessie] Issue with behavior in contracts
- From: dmentre at linux-france.org (David MENTRE)
- [Frama-c-discuss] [Jessie] Issue with behavior in contracts
- References:
- [Frama-c-discuss] [Jessie] Issue with behavior in contracts
- From: dmentre at linux-france.org (David MENTRE)
- [Frama-c-discuss] [Jessie] Issue with behavior in contracts
- Prev by Date: [Frama-c-discuss] RE : [Jessie] Issue with behavior in contracts
- Next by Date: [Frama-c-discuss] [Jessie] Issue with behavior in contracts
- Previous by thread: [Frama-c-discuss] [Jessie] Issue with behavior in contracts
- Next by thread: [Frama-c-discuss] [Jessie] Issue with behavior in contracts
- Index(es):