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

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