Rationale for Ada 2012

John Barnes

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 objectX 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.