1pragma SPARK_Mode;
2package Allocator2 is
3    type Nat_Array is array (Positive range <>) of Natural with
4      Default_Component_Value => 0;
5    type Nat_Stack (Max : Natural) is record
6       Content : Nat_Array (1 .. Max);
7    end record;
8    type Stack_Acc is access Nat_Stack;
9    type My_Rec is private;
10private
11    type My_Rec is record
12       My_Stack : Stack_Acc := new Nat_Stack (Max => 10);
13    end record;
14   procedure Dummy;
15end Allocator2;
16