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



Hello Boris,

Le mer. 10 juin 2009 13:55:35 CEST,
"Hollas Boris (CR/AEY1)" <Boris.Hollas at de.bosch.com> a ?crit :

> 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
> 

You're right that both predicates are not equivalent (and that it is
quite ugly), but \valid_range(a,-1,-2) is not always false. Namely, with

int a[3];
int main() {
int* p=&a[2];
//@ assert \valid_range(p,-1,-2);
return 0;
}

the assertion is true: we have \offset_min(p) = -2, \offset_max(p) = 0
thus
\valid_range(p,-1,-2) <==> \offset_min(p) <= -1 && \offset_max(p) >= -2
                      <==> -2 <= -1 && 0 >= -2 <==> \true
On the other hand, \valid_range(p,0,-1) is false.

BTW, I've summed up a lenghtier answer to your bug report in the wiki:
http://bts.frama-c.com/dokuwiki/doku.php?id=mantis:frama-c:issue:156

> \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

In fact, the definition given by the jessie plugin of \valid_range is
not exactly the informal one which existed before ACSL was published,
which was roughly \forall integer i; l <= i <= r ==> \valid(a+i). I'd
rather be in favor of keeping the definition of \valid as it is now,
without making a particular case for the empty set, and adapting the one
of \valid_range, which is definitively broken. In
terms of \offset_min and \offset_max, this could give
\valid_range(a,l,r) <==> 
  (l<=r ==> \offset_min(a) <= l && \offset_max(a) >= r)

Best regards,
-- 
E tutto per oggi, a la prossima volta.
Virgile