--- layout: fc_discuss_archives title: Message 36 from Frama-C-discuss on December 2008 ---
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