5271925ba5
Currently the syscall invocations may throw away error information in an unretrievable way if they attempt to avoid using the IPC buffer
43 lines
1.3 KiB
Text
43 lines
1.3 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_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
|