GNATprove miscomputes Global aspect for generic formal parameter

[daniel-larraz]

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

[ptroja]

Hi Daniel,

thanks for reporting this. The workaround is to annotate Generic_P with explicit Global => C contract. This is a known issue in GNATprove when generating Global contracts that involve generic formal parameters of mode in. There is no need to report it to the GNAT team.