Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] [Jessie] pset_disjoint

On Jun 10, 2009, at 8:50 AM, Hollas Boris (CR/AEY1) wrote:
>
>> 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.

This is not a feature of ACSL. The separation predicate is an assumption
made (and documented) by Jessie in the hope that it will simplify  
treatment
without being restrictive. The meaning of an ACSL contract where no
\separated appears still is that the pointers do not have to be  
separated,
as you say.

ACSL properties are used both as input and output of plug-ins. In this
case Jessie generates the separation property, to be verified by itself
or another plug-in.

Pascal