--- layout: fc_discuss_archives title: Message 35 from Frama-C-discuss on June 2009 ---
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