--- layout: fc_discuss_archives title: Message 36 from Frama-C-discuss on December 2008 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Safety Conditions in Frama-C



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