Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Validating pointers

  • Subject: [Frama-c-discuss] Validating pointers
  • From: barbaraisabelvieira at gmail.com (Bárbara Vieira)
  • Date: Wed, 1 Jul 2009 15:29:20 +0100
  • In-reply-to: <4A4B6E12.2030802@cea.fr>
  • References: <002701c9fa3c$6fc716b0$4f554410$@com> <4A4B6E12.2030802@cea.fr>
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