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




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                    |