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

On Wed, Mar 4, 2009 at 12:46, Claude March? <Claude.Marche at inria.fr> wrote:
> 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];

Ok.

> More importantly, your use of behaviors is unfortunately wrong.

Ouch!!

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

Ok.

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

Yes.

> ?> ? ?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 :

Yes.

> ? \result == 0 ==>
> ? ? ?global_error_number == \old(global_error_number)
> ? ?&&
> ? ? ?forall integer i; 0 <= i < count ==> buf[i] == \old(buf[i])

Ok.

> (by the way, is it true that read() does not modify errno in case of
> success ? is it guaranteed ?)

I don't know. :-) Good question. I'll check that.

> ?> ? ? 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...)

In fact, the "buf" is declare as "void*" so I was assuming my
properties could not be proved because of that. But in sight of what
you said before, I might be totally wrong.


> 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

That is what I was trying to do. Apparently the wrong way. :-)

Thank you for your explanations. I'll digest that and try to see how I
could improve my specs.

Are there examples anywhere of ACSL specifications that consider
different case depending on the return value of the function,
typically error case and normal one? I assume the things I want to
specify are a recurrent pattern in the use of Frama-C / Jessie.

Sincerely yours,
david