--- layout: fc_discuss_archives title: Message 23 from Frama-C-discuss on March 2009 ---
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