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

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