--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on June 2009 ---
valid and indeed it's more elegant than a definition which considers \valid= (\empty) as a special case. The present definition however allows \valid(s) to be true even if there is= no pointer in s that can be dereferenced. This is no problem if the elemen= ts of s are accessed inside a for-loop that iterates through s. In other si= tuations however you have to be aware that s can be empty and it may be nec= essary to add another precondition. Otherwise, I think it is easy to overlo= ok bugs that stem from an empty set of valid pointers. I suggest to point this out more clearly in the documentation. Maybe someon= e can add a note on \valid(a+(l..r)) in the ACSL reference and give an exam= ple on the tutorial where a[l] may be an invaild access. Concerning \valid_range, I don't see why this predicate is necessary. I thi= nk it just makes it more difficult for the user as he has to read both the = definitions of \valid and \valid_range and ponder what the difference is. How about removing \valid_range? In this case, the user can define his own = predicate, eg \valid_range(a,l,r) <=3D=3D> l < r && \valid(a+(l..r)) Regards, Boris