Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

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