#
# Copyright 2017, Data61
# Commonwealth Scientific and Industrial Research Organisation (CSIRO)
# ABN 41 687 119 230.
#
# This software may be distributed and modified according to the terms of
# the BSD 2-Clause license. Note that NO WARRANTY is provided.
# See "LICENSE_BSD2.txt" for details.
#
# @TAG(DATA61_BSD)
#

menuconfig LIB_SEL4_VKA
    bool "libsel4vka"
    depends on HAVE_LIB_SEL4 && HAVE_LIBC && HAVE_LIB_UTILS
    select HAVE_SEL4_LIBS
    select HAVE_LIB_SEL4_VKA
    default y
    help
        Virtual kernel allocator interface, for allocating memory, untyped memory and cslots.

config LIB_VKA_ALLOW_MEMORY_LEAKS
    bool "Leak memory on free"
    depends on LIB_SEL4_VKA
    default n
    help
        Changes the default free functions to silently leak memory
         instead of assert failing.
         This is useful in scenarios where code is correctly freeing
         resources, but you want to use an allocator that does not
         implement free.

config LIB_SEL4_VKA_DEBUG_LIVE_SLOTS_SZ
    int "(debug allocator) live slot buffer size"
    depends on LIB_SEL4_VKA
    default 0
    help
        VKA contains an allocator, debugvka, that wraps a target VKA allocator
        for the purposes of debugging. It tracks slot and object allocations
        and catches both caller problems like double free, and allocator
        problems like handing out the same resource twice. This configuration
        option sets the maximum number of CSlots that can be tracked at any one
        time.

config LIB_SEL4_VKA_DEBUG_LIVE_OBJS_SZ
    int "(debug allocator) live object buffer size"
    depends on LIB_SEL4_VKA
    default 0
    help
        As for the above option, but sets the maximum number of objects that
        can be tracked at any one time.

config HAVE_LIB_SEL4_VKA
    bool