--- layout: fc_discuss_archives title: Message 116 from Frama-C-discuss on December 2009 ---
[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