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



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.