--- layout: fc_discuss_archives title: Message 37 from Frama-C-discuss on June 2009 ---
Consider an array a[n], n >= 0. Then, for integers l,r we have \valid(a+(l..r)) \neq \valid_range(a,l,r) (*) because \valid(a+(-1..-2) = \valid(\empty) = true but \valid_range(a,-1,-2) = \offset_min(p) <= -1 \land \offset_max(p) >= -2 = false I think it would be much nicer if we had equality in (*). I stumbled on this when I found out that Jessie couldn't verify pointer dereferencing in this code: /*@ requires \valid(a+ (l..r)); */ void foo(int a[], int l, int r) { int k; k = a[r]; // problem here } The reason is that the precondition holds if l > r, in which case any access to a[] may be invalid. However, this is not the behavior I expected. There is an implicit precondition 0 <= l, but no implicit precondition l <= r. But calling a function that expects an array and a range of array indices with an empty range is odd. There's no point in requiring a set of pointers to be valid if there is no pointer in this set that can be dereferenced. I thinks that this is a source of confusion and problems among users. Would it be better to change the semantics of \valid and \valid_range: \valid(s) holds if and only if s \ne \empty and dereferencing any p \in s is safe \valid_range(a,i,j) = \offset_min(p) <= i \land \offset_max(p) >= j \land i <= j Regards, Boris