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