genode/repos/libports/src/test/spark_secondary_stack/stack.ads

46 lines
950 B
Ada

package Stack
with SPARK_Mode
is
type Buffer is array (Integer range <>) of Character;
procedure Calloc (
Size : Integer
);
procedure Ralloc;
function Alloc (
Size : Integer
) return Buffer;
function Recursive_Alloc (
Round : Integer
) return Buffer;
procedure Salloc;
function Stage_1 (
Size : Integer
) return Buffer;
function Stage_2 (
Size : Integer
) return Buffer;
function Stage_3 (
Size : Integer
) return Buffer;
private
procedure Print_Stage (
Stage : Integer
)
with
Import,
Convention => C,
External_Name => "print_stage";
end Stack;