--- layout: fc_discuss_archives title: Message 5 from Frama-C-discuss on June 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

No subject



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