--- layout: fc_discuss_archives title: Message 115 from Frama-C-discuss on December 2009 ---
Hello, > 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)? The first and foremost difference is the same as between a const attribute for the type pointed to by a function's argument and an assigns clause that expresses that the pointed object is not modified: the former is assumed but rarely checked by the compiler (there certainly isn't any guarantee that any write access to a const object will be detected at compile- or even run-time). The latter is a property that is checked of the function, and then used when analyzing callers, in a consistent fashion. Because the intended use is different, the property, while similar, is expressed a little differently, in a more compositional way in the latter case. Another difference is that if you look at restrict as a predicate, is that it's a unary predicate. It expresses that a pointer is (initially, as the function is entered) the only way to reach the pointed object. \separated applies to two pointers and expresses that these two pointers do not point to areas with any aliases between them. The latter may therefore be a little more cumbersome to use (making it necessary to express many pairwise separation properties). The former is more expressive when it applies, but there are some corner cases where it is unable to capture the aliasing situation. This distinction reflects the difference in purpose between an attribute intended to allow most of the time to express properties allowing optimization with the lowest possible demand on the developer, on the one hand, and a predicate intended to capture precisely the formal specification of any reasonable C function on the other hand. Pascal