Rationale for Ada 2012
2.7 Storage occupancy checks
Finally, two new attributes are introduced to aid
in the writing of preconditions. Sometimes it is necessary to check that
two objects do not occupy the same storage in whole or in part. This
can be done with two functional attributes
X'Has_Same_Storage
and
X'Overlaps_Storage which apply to an object
X
of any type.}
Their specifications
are
function X'Has_Same_Storage(Arg: any_type) return Boolean;
function X'Overlaps_Storage(Arg: any_type) return Boolean;
As an example we might
have a procedure Exchange and wish to ensure
that the parameters do not overlap in any way. We can write
procedure Exchange(X, Y: in out T)
with Pre => not X'Overlaps_Storage(Y);
Attributes are used rather than predefined functions
since this enables the semantics to be written in a manner that permits
X and Y to be of
any type and moreover does not imply that X
or Y are read.
The object X and the parameter
Y could be components such as A(5)
or indeed A(J) or even a slice A(1
.. N). Thus the actual addresses to be checked may not be statically
determined but have to be determined at the point of call.
AI-191
shows the following curious example
procedure Count(A: in out Arrtype; B: in Arrtype)
with Pre => not A'Overlaps_Storage(B)
is
-- intended to count in A the number of value
-- occurrences in B as part of a distribution sort
begin
for I in B'Range loop
A(B(I)) := A(B(I)) + 1;
end loop;
end Count;
The author seems to have assumed that the array A
has appropriate components and that they are initialized to zero. This
also illustrates the use of an aspect specification in a subprogram body.
At the machine level Overlaps_Storage
means that at least one bit is in common and Has_Same_Storage
means that all bits are in common. Hence X'Has_Same_Storage(Y)
implies X'Overlaps_Storage(Y).
In some applications involving the possibility of
aliasing (messing with tree structures comes to mind) we do really want
to check that two entities are not in the same place rather than just
overlapping in which case it is more logical to use Has_Same_Storage.
© 2011, 2012, 2013 John Barnes Informatics.
Sponsored in part by: