#
# 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

choice
    prompt "Function attributes"
    default LIB_SEL4_INLINE_INVOCATIONS

config LIB_SEL4_DEFAULT_FUNCTION_ATTRIBUTES
    bool "Default"
    depends on LIB_SEL4
    help
        Verification friendly default configuration. syscalls will be inlined,
        but generated functions will not.

config LIB_SEL4_INLINE_INVOCATIONS
    bool "Inline generated syscall invocations"
    depends on LIB_SEL4
    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 forcibly prevent the function
        from being inlined.

config LIB_SEL4_PUBLIC_SYMBOLS
    bool "Public symbols for all external interfaces"
    depends on LIB_SEL4
    help
        When set to true will make all user facing functions available as
        public symbols, which can be convenient for some language bindings.

endchoice

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.

config HAVE_LIB_SEL4
    bool
endmenu
