--- layout: fc_discuss_archives title: Message 23 from Frama-C-discuss on November 2010 ---
On Fri, 2010-11-12 at 13:54 +0100, Jens Gerlach wrote: > I want to write a simple get-function for a struct that contains a > fixed-size array. > It seems, however, that Frama-C (or Jessie?) does not recognise that the > array is a valid range. > Did I forget something obvious, is it a known bug, or should I create an > entry to the BTS? > > Regards > > Jens > > > 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. -- Regards, Boris