--- layout: fc_discuss_archives title: Message 18 from Frama-C-discuss on March 2009 ---
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; > ?*/ > // ?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?