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 and -no-regions

Thanks for your remarks on "\separated" and "restrict", Pascal.

The \separated clause is marked as experimental in the ACSL specification document
and, as far as I can see, it is not supported by Frama-C.
Jessie, on the other hand, assumes that different pointers point to different "regions".

Does this mean that Jessie assumes for two pointers a and b that
	\base_addr(a) != \base_addr(b)
holds?

I no that Jessie's default behavior can be changed with the option "-jessie-no-regions".
However, I would rather have the behavior of -jessie-no-regions" by default and 
an explicit option for the complementary case (maybe "-jessie-assumes-separated") because
the current default treatment  of pointers by Jessie deviates from the C standard.


Regards Jens