Re: Assertion_Policy implementation regarding Aspect Features

[Simon Wright <simon@pushface.org>]

Anh Vo <anhvofrcaus@gmail.com> writes:

> This inspires me to learn this feature a little bit deeper. I would
> like to know if GNAT comply with ARM by showing the following
> scenarios.

The fact that you need to enable assertions with -gnata seems to be a
GNAT feature, so we'll maybe need to add -gnata to the other flags
needed to make GNAT a standard-conforming compiler (-fstack-check,
-gnato).

I don't see in the ARM anything that says what the default
Assertion_Policy should be.

On the other hand, the fact that your predicate isn't disabled by pragma
Assertion_Policy (Ignore) may be a failure to comply with the second
sentence of ARM 11.4.2(10)[1]:

   The policy_identifier Check requires that assertion expressions of
   the given aspect be checked that they evaluate to True at the points
   specified for the given aspect; the policy_identifier Ignore requires
   that the assertion expression not be evaluated at these points, and
   the run-time checks not be performed.

because of a misinterpretation of the last sentence:

   Note that for subtype predicate aspects (see 3.2.4), even when the
   applicable Assertion_Policy is Ignore, the predicate will still be
   evaluated as part of membership tests and Valid attribute_references,
   and if static, will still have an effect on loop iteration over the
   subtype, and the selection of case_statement_alternatives and
   variants.

[1] http://www.ada-auth.org/standards/12rm/html/RM-11-4-2.html#p10