pragma SPARK_Mode;
package Allocator2 is
    type Nat_Array is array (Positive range <>) of Natural with
      Default_Component_Value => 0;
    type Nat_Stack (Max : Natural) is record
       Content : Nat_Array (1 .. Max);
    end record;
    type Stack_Acc is access Nat_Stack;
    type My_Rec is private;
private
    type My_Rec is record
       My_Stack : Stack_Acc := new Nat_Stack (Max => 10);
    end record;
   procedure Dummy;
end Allocator2;