be68b0c0bd
Reintroduces Kconfig option removed in 5271925ba5
that allows invocations to use the WithMRs variants of syscalls instead of
using the IPC buffer
41 lines
1.1 KiB
Text
41 lines
1.1 KiB
Text
#
|
|
# 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_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
|