--- layout: fc_discuss_archives title: Message 16 from Frama-C-discuss on November 2010 ---
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]; }