--- layout: fc_discuss_archives title: Message 52 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



>As a minor remark about \valid_range, I would like to add that I find it always a bit odd
>that I have to specify


>\valid_range(a, 0, n-1)


>to express an array of length n. I would prefer "\valid_range(a, 0, n)"  or even shorter "\valid_range(a, n)".
>In other words, I think that right open ranges fit better to C.


The same is true for \valid, you have to specify \valid(a+(0..n-1)).

However, I prefer it this way. I believe it makes the range of indices more explicit.

Spec# has a range operator (0:a.Length) = {k | 0 <= k < a.Length}. I find it a bit confusing that the first element is included in the range, but not the last.


If however \valid_range is not part of ACSL every user can define it in a way he preferes.

Regards,
Boris