#
# 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_INLINE_INVOCATIONS
    bool "Inline generated syscall invocations"
    depends on LIB_SEL4
    default y
    help
        When set to true will mark generated functions as 'inline', allowing
        them to be inlined by the callee user code. This may be undesirable
        for verification, so setting to 'n' will forcively prevent the function
        from being inlined

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

config HAVE_LIB_SEL4
    bool
endmenu
