--- layout: fc_discuss_archives title: Message 18 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,

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?