1/* 2 * Copyright 2014, General Dynamics C4 Systems 3 * 4 * SPDX-License-Identifier: GPL-2.0-only 5 */ 6 7#include <assert.h> 8#include <arch/machine/registerset.h> 9 10const register_t msgRegisters[] = { 11 R2, R3, R4, R5 12}; 13compile_assert( 14 consistent_message_registers, 15 sizeof(msgRegisters) / sizeof(msgRegisters[0]) == n_msgRegisters 16); 17 18const register_t frameRegisters[] = { 19 FaultIP, SP, CPSR, 20 R0, R1, R8, R9, R10, R11, R12 21}; 22compile_assert( 23 consistent_frame_registers, 24 sizeof(frameRegisters) / sizeof(frameRegisters[0]) == n_frameRegisters 25); 26 27const register_t gpRegisters[] = { 28 R2, R3, R4, R5, R6, R7, R14, 29 TPIDRURW, TPIDRURO 30}; 31compile_assert( 32 consistent_gp_registers, 33 sizeof(gpRegisters) / sizeof(gpRegisters[0]) == n_gpRegisters 34); 35 36#ifdef CONFIG_KERNEL_MCS 37word_t getNBSendRecvDest(void) 38{ 39 return getRegister(NODE_STATE(ksCurThread), nbsendRecvDest); 40} 41#endif 42