#
# Copyright 2014, NICTA
#
# 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(NICTA_BSD)
#

menu "libsel4"
    config LIB_SEL4
        bool "libsel4"
        default y
        select HAVE_LIB_SEL4
        help
            seL4 API library

config LIB_SEL4_HAVE_REGISTER_STUBS
    bool "Support syscall stubs without IPC buffer"
    depends on LIB_SEL4 && !USER_OPTIMISATION_O0 && ARCH_ARM
    default y
    help
        Generate the 'WithMRs' variants of the syscall stubs. These stubs
        avoid the use of the IPC buffer where possible and attempt to
        place syscall arguments directly into and out of cpu registers.
        GCC's register allocation is a hint only and cannot be relied upon,
        as a result these stubs are known to be broken, and are disabled,
        at -O0

if LIB_SEL4_HAVE_REGISTER_STUBS || !(ARCH_ARM)
config LIB_SEL4_STUBS_USE_IPC_BUFFER_ONLY
    bool "use only IPC buffer for syscalls"
    depends on LIB_SEL4
    default n
    help
        When generating syscall wrappers, only use the IPC buffer for
        marshalling and unmarshalling arguments. Without this option set,
        arguments will be passed in registers where possible for better
        performance.
endif

if !(LIB_SEL4_HAVE_REGISTER_STUBS || !(ARCH_ARM))
menu "libsel4 hidden"
    visible if false
    config LIB_SEL4_STUBS_USE_IPC_BUFFER_ONLY
        bool "Use only IPC buffer for syscalls"
        depends on LIB_SEL4
        default y
endmenu
endif

config HAVE_LIB_SEL4
    bool
endmenu
