--- layout: fc_discuss_archives title: Message 33 from Frama-C-discuss on June 2009 ---
Hello Boris, Le mar. 09 juin 2009 17:13:17 CEST, "Hollas Boris (CR/AEY1)" <Boris.Hollas at de.bosch.com> a ?crit : > I'm unable to verify the code below. It seems that Jessie requires that p and q are pointers to distinct memory locations. However, this is not required by Copy. > Is this a bug? > No, this is a feature ;-). In fact, the default behavior of jessie is indeed to consider that the arguments of a function points to distinct memory locations. This usually greatly simplifies the proof obligations (when you write something in *p you know that *q is still the same). But of course this is a new implicit pre-condition, and like user-defined pre-conditions it must be checked for each call. You can disactivate this behavior by giving the option -jessie-no-region to Frama-C. Best regards, -- E tutto per oggi, a la prossima volta. Virgile