--- layout: fc_discuss_archives title: Message 16 from Frama-C-discuss on March 2009 ---
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); The "complete" clause is commented-out as Jessie does not support it. The error behaviour states the error case, when \result < 0 and thus only a global error number is assigned. The end_of_file behaviour states the case when \result==0, nothing is assigned. The normal behaviour states the case when some characters are returned, the buffer is assigned and the first character is a byte (it would be useful to specify that buf[0..count-1] is assigned with bytes, but as far as I know Jessie does not support \lambda construct). The code seems to work, as I am able to prove some properties and assertions in my code with Alt-Ergo. 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? If not, how can I write the contract to specify what I mean? Should I use other forms for logical formula? Please find attached the complete source code. Sincerely yours, david -------------- next part -------------- A non-text attachment was scrubbed... Name: dev-random-pass-gen.c Type: application/octet-stream Size: 5365 bytes Desc: not available Url : http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090303/f4eb48bf/attachment-0002.obj -------------- next part -------------- A non-text attachment was scrubbed... Name: check_specs.h Type: application/octet-stream Size: 1253 bytes Desc: not available Url : http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090303/f4eb48bf/attachment-0003.obj