--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on July 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Validating pointers



Hi B?rbara,
> To validate the pre-conditions on "g", I have to assume that: 
>
> *\valid*(e) && *\valid*(e->a) && *\valid*(&(e->a));
>
> My question is, why I have to assume *\valid*(&(e->a)) ?
>
This seems to be a lack of Jessie.
>
> Assuming just that *\valid*(e) && *\valid*(e->a) is not sufficient?
>
Yes it should be from an ACSL point of view.
>
> If I assume that e!=NULL && e->a!=NULL, this does not implies that 
> &(e->a) != NULL?
>
Just a warning, *\valid*(e) is stronger than e!=NULL since *\valid*(e) 
speaks also about the liveness and the size of the pointed location.

But anyway *\valid*(e) => *\valid*(&(e->a)) is  a valid ACSL theorem 
when the formula is correctly type-checked and the type of (*e) isn't a 
incomplete struct/union type.

Patrick.

-- 
Patrick Baudin,
CEA, LIST, SOL, 91191 Gif-surYvette cedex, France.
tel: +33 (0)1 6908 2072

-------------- section suivante --------------
Une pi?ce jointe HTML a ?t? enlev?e...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090701/f8394f9c/attachment.htm