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