--- layout: fc_discuss_archives title: Message 32 from Frama-C-discuss on November 2010 ---
Yes, it works with the additional requires. I have already submitted an entry to BTS. Interestingly, all "safety proof obligations" are proven for the original specification. Thus, it does seem to recognize that s->array[i] is a valid memory access for 0 <= i < 2 . Regards Jens On 15.11.10 16:08, "Boris Hollas" <hollas at informatik.htw-dresden.de> wrote: >> >> struct S >> { >> int array[3]; >> }; >> >> typedef struct S S; >> >> /*@ >> requires \valid(s); >> requires 0 <= i < 3; >> >> assigns \nothing; >> >> ensures \result == s->array[i]; >> */ >> int get(S* s, int i) >> { >> //@ assert \valid_range(s->array, 0, 2); >> return s->array[i]; >> } > > Does > > requires \valid(s) && \valid(s->array+(0..2)); > > work? > > Each time a structure s of type S is created, the member int array[3] is > also created. Therefore, the validity of s should imply the validity of > s->array+(0..2). If Jessie doesn't recognized this, it's a bug.