--- layout: fc_discuss_archives title: Message 16 from Frama-C-discuss on November 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] arrays in struct



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];
}