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] Safety Conditions in Frama-C

  • Subject: [Frama-c-discuss] Safety Conditions in Frama-C
  • From: barbaraisabelvieira at gmail.com (Bárbara Vieira)
  • Date: Sat, 13 Dec 2008 21:01:55 -0000
  • In-reply-to: <75A751E7-12B6-4DFE-91F8-26770FCEE4C5@first.fraunhofer.de>
  • References: <A7A523FB-A98A-46CF-B212-35FC882494EB@first.fraunhofer.de> <75A751E7-12B6-4DFE-91F8-26770FCEE4C5@first.fraunhofer.de>
Thanks Jens. I has understood! 

 

Thanks for your helping.

Best regards,

B?rbara

 

 

From: Jens Gerlach [mailto:jens.gerlach at first.fraunhofer.de] 
Sent: s?bado, 13 de Dezembro de 2008 13:58
To: B?rbara Vieira
Subject: Fwd: [Frama-c-discuss] Safety Conditions in Frama-C

 

 

 

Anfang der weitergeleiteten E-Mail:





Von: Jens Gerlach <jens.gerlach at first.fraunhofer.de>

Datum: 11. Dezember 2008 21:28:30 MEZ

An: frama-c-discuss at lists.gforge.inria.fr

Betreff: Re: [Frama-c-discuss] Safety Conditions in Frama-C

 

Hi B?rbara,

 

I am not a language lawyer for C, but regarding pointer addition the C standard says in section 6.5.6 paragraph 8:

 

                If both the pointer operand and the result point to elements of the same array object, or one past the last 

                element of the array object, the evaluation shall not produce an over?ow; otherwise, the behavior is unde?ned.

 

So I think the behavior of your code is undefined and I would expect proves for undefined behavior.

 

Here is a typo: I meant of course "I would not expect any proves for undefined behavior"

 

Jens

 

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081213/c98a4585/attachment.htm