--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on July 2009 ---
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