From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham
	autolearn_force=no version=3.4.4
X-Google-Thread: 103376,2901996ead8d0ecd
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,ASCII-7-bit
X-Received: by 10.180.82.1 with SMTP id e1mr1272304wiy.1.1360405476099;
        Sat, 09 Feb 2013 02:24:36 -0800 (PST)
Path: 
 g1ni540wig.0!nntp.google.com!feeder1-2.proxad.net!proxad.net!feeder1-1.proxad.net!ecngs!feeder2.ecngs.de!feeder.erje.net!eu.feeder.erje.net!eternal-september.org!feeder.eternal-september.org!.POSTED!not-for-mail
From: Simon Wright <simon@pushface.org>
Newsgroups: comp.lang.ada
Subject: Re: Assertion_Policy implementation regarding Aspect Features
Date: Sat, 09 Feb 2013 10:24:41 +0000
Organization: A noiseless patient Spider
Message-ID: <ly6221ss2e.fsf@pushface.org>
References: <dd938cdd-f00d-413a-8d1c-b4e7f140c7ab@googlegroups.com>
Mime-Version: 1.0
Injection-Info: mx05.eternal-september.org;
 posting-host="0a6ca0935c728e617c1a2d4bdcfc6a33";
	logging-data="13697"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX1/vfDpVkWGXqKv4BNQ2tUaNSKLVbGbj4V8="
User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/24.2 (darwin)
Cancel-Lock: sha1:GKS2RZcmjIOR37UDZRJwiukPCNk=
	sha1:9SqId218sYzy+PMCsLXay4JD2ws=
Content-Type: text/plain
Date: 2013-02-09T10:24:41+00:00
List-Id: <comp.lang.ada>

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