--- layout: fc_discuss_archives title: Message 34 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 Virgile,

>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

Of course, in most cases, this makes sense and prevents a lot of bugs. But I haven't found this in the ACSL documentation. Since distinct memory locations can be expressed with the separated predicate, I assumed that pointers don't have to be distinct by default.

Best regards,
Boris