Overview of Ada 2022
3.7 Other support for pre- and postconditions
Pre/Post for access-to-subprogram
types (AI12-0220)
allows Pre and Post aspects for access-to-subprogram types, so that contract
information is available when calling a subprogram indirectly via an
access value, as well as (or even instead of) when called directly. For
example, to check that a parameter is even:
type T1 is access procedure (X : Integer)
with Pre => X mod 2 = 0;
procedure Foo (X : Integer) is ... end;
...
Ptr1 : T1 := Foo'Access;
begin
Ptr1.all (222); -- Precondition check performed
Making 'Old more flexible (AI12-0280-2).
Currently the following is illegal as the
A.all
in
A.all'Old is “potentially
unevaluated”:
procedure Proc (A : access Integer)
with Post =>
(if A /= null then (A.all'Old > 1 and A.all > 1));
This is now relaxed. Thinking less of what it may
not be possible to evaluate, but more of what can be evaluated
in advance, the term “known on entry” is introduced to cover
such expressions (the most obvious example being a static expression),
and if it is possible to tell on entry to a subprogram that an X'Old
need not be evaluated then it isn't. In the example, A
is an in parameter of an elementary type (which includes access
types) so it is passed by copy and cannot change, so if A
is null on entry then A.all'Old
would not be evaluated.
© 2021, 2022 Jeff Cousins