Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[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                    |