--- layout: fc_discuss_archives title: Message 35 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



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