[Bug ada/105303] Assertion_Policy (Pre => Ignore) executes precondition

cvs-commit at gcc dot gnu.org gcc-bugzilla@gcc.gnu.org
Mon May 30 08:29:57 GMT 2022


https://gcc.gnu.org/bugzilla/show_bug.cgi?id=105303

--- Comment #2 from CVS Commits <cvs-commit at gcc dot gnu.org> ---
The master branch has been updated by Pierre-Marie de Rodat
<pmderodat@gcc.gnu.org>:

https://gcc.gnu.org/g:5b7630f2f266346173eb2172a9a96e925010afc5

commit r13-826-g5b7630f2f266346173eb2172a9a96e925010afc5
Author: Yannick Moy <moy@adacore.com>
Date:   Tue Apr 19 14:37:58 2022 +0200

    [Ada] PR ada/105303 Fix use of Assertion_Policy in internal generics unit

    The internal unit System.Generic_Array_Operations defines only generic
    subprograms. Thus, pragma Assertion_Policy inside the spec has no
    effect, as each instantiation is only subject to the assertion policy at
    the program point of the instantiation. Remove this confusing pragma,
    and add the pragma inside each generic body making use of additional
    assertions or ghost code, so that running time of instantiations is not
    impacted by assertions meant for formal verification.

    gcc/ada/

            PR ada/105303
            * libgnat/s-gearop.adb: Add pragma Assertion_Policy in generic
            bodies making use of additional assertions or ghost code.
            * libgnat/s-gearop.ads: Remove confusing Assertion_Policy.


More information about the Gcc-bugs mailing list