Instantiating non-library-level package in SPARK Ada

Question

How do I instantiate a non-library-level package in SPARK Ada?

Say I have something like:

subtype Die is Integer range 1..6;
package Random_Die
is
  new Ada.Numerics.Discrete_Random(Die);

That gives me the errors:

instantiation error at a-nudira.ads.45
incorrect placement of "Spark_Mode"
Random_Die is not a libray level package

Presumably I need to turn SPARK_Mode off for Ada.Numerics.Discrete_Random, but I can't work out the right place to put the pragma.

Answer 1

Generics are only checked by SPARK when they are instantiated. :-(

The error message looks like you have attempted to put a SPARK_Mode aspect somewhere inside the generic. That will not work. You should put the SPARK_Mode => On aspect on the unit instantiating the generic package.

Answer 2

The message isn't so much about Ada.Numerics.Discrete_Random. Spark-2014 wants you to make your unnamed package, Unnamed, say, to be at library level, like Jacob Sparre Andersen mentions in his answer. To wit:

with Ada.Numerics.Discrete_Random;

--procedure Outer is
   package Unnamed
      with Spark_Mode => On
   is
      subtype Die is Integer range 1..6;
      package Random_Die
      is
        new Ada.Numerics.Discrete_Random(Die);
   end Unnamed;
--begin
--   null;
--end Outer;

Removing the comments' hyphens and translating Outer yields your error message. Translating Unnamed as is will work fine, and gnatprove has no complaints. In other words, Unnamed is then a library level package. Within Outer it isn't and this makes GNAT issue the diagnostic message.