--- layout: fc_discuss_archives title: Message 33 from Frama-C-discuss on June 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] [Jessie] pset_disjoint



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