--- layout: fc_discuss_archives title: Message 23 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



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