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

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

[simon at pushface dot org]

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

            Bug ID: 105303
           Summary: Assertion_Policy (Pre => Ignore) executes precondition
           Product: gcc
           Version: 12.0
            Status: UNCONFIRMED
          Severity: normal
          Priority: P3
         Component: ada
          Assignee: unassigned at gcc dot gnu.org
          Reporter: simon at pushface dot org
  Target Milestone: ---

System.Generic_Array_Operations starts with

   --  Preconditions in this unit are meant for analysis only, not for run-time
   --  checking, so that the expected exceptions are raised. This is enforced
   --  by setting the corresponding assertion policy to Ignore. Postconditions
   --  and contract cases should not be executed at runtime as well, in order
   --  not to slow down the execution of these functions.

   pragma Assertion_Policy (Pre            => Ignore,
                            Post           => Ignore,
                            Contract_Cases => Ignore,
                            Ghost          => Ignore);

and yet, given this clearly wrong code (compiled with -gnata)

   with System.Generic_Array_Operations;
   procedure Transposition is
      type Matrix is array (Integer range <>, Integer range <>) of Float;
      procedure Transpose is new System.Generic_Array_Operations.Transpose
        (Scalar => Float,
         Matrix => Matrix);
      Input : Matrix (1 .. 3, 1 .. 4);
      Output : Matrix (1 .. 3, 1 .. 2);
   begin
      Transpose (Input, Output);
   end Transposition;

Ada.Assertions.Assertion_Error is in fact raised, contrary to ARM2012
11.4.2(10):

   $ ./transposition 

   raised ADA.ASSERTIONS.ASSERTION_ERROR : failed precondition from
s-gearop.ads:569 instantiated at transposition.adb:4

The comment noted above is confusing, if not wrong:

"Preconditions ... not meant for runtime checking, so that the expected
exceptions are raised" -- the checks should not be performed, and the
exceptions should not be raised.

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

[ebotcazou at gcc dot gnu.org]

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

Eric Botcazou <ebotcazou at gcc dot gnu.org> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
     Ever confirmed|0                           |1
   Last reconfirmed|                            |2022-04-20
                 CC|                            |ebotcazou at gcc dot gnu.org
             Status|UNCONFIRMED                 |NEW

--- Comment #1 from Eric Botcazou <ebotcazou at gcc dot gnu.org> ---
Confusing indeed.

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

[cvs-commit at gcc dot gnu.org]

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.

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

[charlet at gcc dot gnu.org]

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

Arnaud Charlet <charlet at gcc dot gnu.org> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
             Status|NEW                         |RESOLVED
                 CC|                            |charlet at gcc dot gnu.org
         Resolution|---                         |FIXED
   Target Milestone|---                         |13.0

--- Comment #3 from Arnaud Charlet <charlet at gcc dot gnu.org> ---
fixed on master