--- layout: fc_discuss_archives title: Message 20 from Frama-C-discuss on March 2009 ---
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 |