GNATprove miscomputes Global aspect for generic formal parameter

bug.adb

pragma Spark_Mode (On);

procedure Bug is

   generic
      type T is private;
      C : T;
   procedure Generic_P (R : out T);

   procedure Generic_P (R : out T) is
   begin
      R := C;
   end Generic_P;

   type Int_Array is array (Natural range <>) of Integer;

   procedure P1 (N : Integer; O : out Integer)
   is
      subtype N_Array is Int_Array (0 .. N);

      procedure P2 is new Generic_P (
         T => N_Array,
         C => [others => 0]
      );

      A : N_Array;
   begin
      P2 (A); O := N;
   end P1;

   O : Integer;
begin
   P1 (4, O);
end Bug;

Running GNATprove:

$ alr gnatprove
Phase 1 of 3: generation of data representation information ...
Phase 2 of 3: generation of Global contracts ...
Phase 3 of 3: flow analysis and proof ...
+===========================GNAT BUG DETECTED==============================+
| 1.0 (spark) Program_Error Bug.P1 @ 26 : C                                |
| Error detected at bug.adb:28:7                                           |
| Compiling /path/to/bug.adb                                               |
| Please submit a bug report; see https://gcc.gnu.org/bugs/ .              |
| Use a subject line meaningful to you and us to track the bug.            |
| Include the entire contents of this bug box in the report.               |
| Include the exact command that you entered.                              |
| Also include sources listed below.                                       |
+==========================================================================+

Please include these source files with error report
Note that list may not be accurate in some cases,
so please double check that the problem can still
be reproduced with the set of files listed.
Consider also -gnatd.n switch (see debug.adb).

/path/to/bug.adb


bug.adb:28:07: high: constant with variable input "C" must be listed in the Global aspect of "P1" (SPARK RM 6.1.4(15))
   28 |      P2 (A); O := N;
      |      ^~~~~
compilation abandoned

I am reporting this issue here because it occurs only when running GNATprove and not when building the program. Please let me know whether this should instead be reported to the GNAT developers' team.

Versions:
gnat FSF: 15.2.1
gnatprove: 15.1.0

Start by reproducing the supplied example in bug.adb with alr gnatprove, using the listed GNAT and GNATprove versions. Trace the Phase 2 Global contract generation for the generic formal parameter and compare it with the diagnostic at line 28. Done means GNATprove no longer raises Program_Error and reports the correct Global requirement for this case.