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