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,FREEMAIL_FROM,
	WEIRD_PORT autolearn=unavailable autolearn_force=no version=3.4.4
X-Received: by 10.99.96.209 with SMTP id u200mr11639688pgb.28.1498785353979;
        Thu, 29 Jun 2017 18:15:53 -0700 (PDT)
X-Received: by 10.36.160.9 with SMTP id o9mr185152ite.9.1498785353920; Thu, 29
 Jun 2017 18:15:53 -0700 (PDT)
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!news.eternal-september.org!feeder.eternal-september.org!news.glorb.com!v202no137423itb.0!news-out.google.com!k7ni3877itk.0!nntp.google.com!v202no137422itb.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail
Newsgroups: comp.lang.ada
Date: Thu, 29 Jun 2017 18:15:53 -0700 (PDT)
Complaints-To: groups-abuse@google.com
Injection-Info: glegroupsg2000goo.googlegroups.com; posting-host=82.8.94.50;
 posting-account=7NSrMAoAAACQXGDiUf5Zzn18ZM31fxb5
NNTP-Posting-Host: 82.8.94.50
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <e3a88437-89a9-4feb-9780-1b06ca32e033@googlegroups.com>
Subject: Can't work out how to use with Ada.Numerics.Discrete_Random with
 SPARK 2014
From: digitig <digitig@gmail.com>
Injection-Date: Fri, 30 Jun 2017 01:15:53 +0000
Content-Type: text/plain; charset="UTF-8"
Xref: news.eternal-september.org comp.lang.ada:47202
Date: 2017-06-29T18:15:53-07:00
List-Id: <comp.lang.ada>

In main.ads I have:

package Main
with SPARK_Mode => On
is
   procedure Test;
end Main;

In main.adb I have:

with Ada.Numerics.Discrete_Random;
with Ada.Text_IO;
package body Main
with SPARK_Mode => On
is
   procedure Test is
      subtype Die is Integer range 1 .. 6;
      subtype Dice is Integer range 2*Die'First .. 2*Die'Last;
      package Random_Die is new Ada.Numerics.Discrete_Random (Die);
      use Random_Die;
      G : Generator;
      D : Dice;
   begin
      Reset (G);  -- Start the generator in a unique state in each run
      loop
         -- Roll a pair of dice; sum and process the results
         D := Random(G) + Random(G);
         Ada.Text_IO.Put_Line(D'Image);
      end loop;
   end Test;
end Main;

Running SPARK | Examine all sources from GPS gives me the error:

        9:7 "Random_Die" is not a library-level package
        9:7 incorrect placement of aspect "Spark_Mode"
        9:7 instantiation error at a-nudira.ads:45

Line 9 is:

      package Random_Die is new Ada.Numerics.Discrete_Random (Die);

But the error points into a line in the GNAT library, in a-nudira.ads that simply says

        SPARK_Mode => Off

I'm completely bewildered here - what's wrong with my code here (other than it being a toy example)? And how *do* I use Ada.Numerics.Discrete_Random in conjunction with SPARK?