1/* 2 * Copyright 2017, Data61 3 * Commonwealth Scientific and Industrial Research Organisation (CSIRO) 4 * ABN 41 687 119 230. 5 * 6 * This software may be distributed and modified according to the terms of 7 * the BSD 2-Clause license. Note that NO WARRANTY is provided. 8 * See "LICENSE_BSD2.txt" for details. 9 * 10 * @TAG(DATA61_BSD) 11 */ 12 13#ifndef __LIBSEL4_SEL4_ARCH_FUNCTIONS_H 14#define __LIBSEL4_SEL4_ARCH_FUNCTIONS_H 15 16#include <autoconf.h> 17#include <sel4/constants.h> 18#include <sel4/sel4_arch/constants.h> 19 20LIBSEL4_INLINE_FUNC seL4_IPCBuffer* 21seL4_GetIPCBuffer(void) 22{ 23#if defined(CONFIG_IPC_BUF_GLOBALS_FRAME) 24 return *(seL4_IPCBuffer**)seL4_GlobalsFrame; 25#elif defined(CONFIG_IPC_BUF_TPIDRURW) 26 seL4_Word reg; 27 asm ("mrc p15, 0, %0, c13, c0, 2" : "=r"(reg)); 28 return (seL4_IPCBuffer*)reg; 29#else 30#error "Unknown IPC buffer strategy" 31#endif 32} 33 34#endif 35