--- layout: fc_discuss_archives title: Message 3 from Frama-C-discuss on July 2009 ---
Hi Patrick, Many thanks for the answer. Best regards, B?rbara From: frama-c-discuss-bounces at lists.gforge.inria.fr [mailto:frama-c-discuss-bounces at lists.gforge.inria.fr] On Behalf Of BAUDIN Patrick Sent: quarta-feira, 1 de Julho de 2009 15:09 To: Frama-C public discussion Subject: Re: [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 __________ Information from ESET Smart Security, version of virus signature database 4204 (20090701) __________ The message was checked by ESET Smart Security. http://www.eset.com -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20090701/db8c0afb/attachment-0001.htm