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