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