blob: 7c4c22838036447619a9dc0a3b75e23ca1c5ab71 [file] [log] [blame]
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;
type My_Rec is record
My_Stack : Stack_Acc := new Nat_Stack (Max => 10);
end record;
procedure Dummy;
end Allocator2;