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]

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