--- layout: fc_discuss_archives title: Message 114 from Frama-C-discuss on December 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] relationship of separated and restrict qualifier



Hi,

the ACSL specification introduces (experimentally) the "\separated" annotation (?2.7.2).
I understand that it serves the purpose of expressing that different pointers point to different memory locations.
Is there a major difference between "\separated" and the "restrict" type qualifier of C99 
(see http://developers.sun.com/solaris/articles/cc_restrict.html)?

Regards Jens