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

[Frama-c-discuss] Semantics of \valid



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