--- layout: fc_discuss_archives title: Message 39 from Frama-C-discuss on June 2009 ---
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