| 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; |