16 lines
453 B
Ada
16 lines
453 B
Ada
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;
|