1

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.

digitig
  • 1,989
  • 3
  • 25
  • 45

2 Answers2

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.

Jacob Sparre Andersen
  • 6,733
  • 17
  • 22
  • The only mention of SPARK_Mode *I* have is the SPARK_Mode => On on the entire package that contains the code I cited. The error message points to a-nudira.ads.45, which says SPARK_Mode => Off, but a-nudira.ads is a standard library module from the GNAT distribution, not my own code. – digitig Jul 01 '17 at 14:37
  • Strange. Then maybe you should simply do as requested, and make the generic instantiation of `Ada.Numerics.Discrete_Random` a library level package. – Jacob Sparre Andersen Jul 02 '17 at 08:55
1

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.

B98
  • 1,229
  • 12
  • 20