1/* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * Copyright 2015, 2016 Hesham Almatary <heshamelmatary@gmail.com> 4 * 5 * SPDX-License-Identifier: GPL-2.0-only 6 */ 7 8#include <assert.h> 9#include <arch/machine/registerset.h> 10 11const register_t msgRegisters[] = { 12 a2, a3, a4, a5 13}; 14compile_assert( 15 consistent_message_registers, 16 sizeof(msgRegisters) / sizeof(msgRegisters[0]) == n_msgRegisters 17); 18 19const register_t frameRegisters[] = { 20 FaultIP, ra, sp, gp, 21 s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, 22}; 23compile_assert( 24 consistent_frame_registers, 25 sizeof(frameRegisters) / sizeof(frameRegisters[0]) == n_frameRegisters 26); 27 28const register_t gpRegisters[] = { 29 a0, a1, a2, a3, a4, a5, a6, a7, 30 t0, t1, t2, t3, t4, t5, t6, 31 tp, 32}; 33compile_assert( 34 consistent_gp_registers, 35 sizeof(gpRegisters) / sizeof(gpRegisters[0]) == n_gpRegisters 36); 37 38#ifdef CONFIG_KERNEL_MCS 39word_t getNBSendRecvDest(void) 40{ 41 return getRegister(NODE_STATE(ksCurThread), nbsendRecvDest); 42} 43#endif 44