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