1/* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 */ 6 7#pragma once 8 9#include <autoconf.h> 10#include <sel4/functions.h> 11#include <sel4/sel4_arch/syscalls.h> 12#include <sel4/types.h> 13 14#ifdef CONFIG_KERNEL_MCS 15LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Poll(seL4_CPtr src, seL4_Word *sender) 16{ 17 return seL4_NBWait(src, sender); 18} 19#else /* CONFIG_KERNEL_MCS */ 20LIBSEL4_INLINE_FUNC void seL4_Wait(seL4_CPtr src, seL4_Word *sender) 21{ 22 seL4_Recv(src, sender); 23} 24LIBSEL4_INLINE_FUNC seL4_MessageInfo_t seL4_Poll(seL4_CPtr src, seL4_Word *sender) 25{ 26 return seL4_NBRecv(src, sender); 27} 28#endif /* !CONFIG_KERNEL_MCS */ 29