1/*
2 * Copyright 2014, NICTA
3 *
4 * This software may be distributed and modified according to the terms of
5 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
6 * See "LICENSE_BSD2.txt" for details.
7 *
8 * @TAG(NICTA_BSD)
9 */
10
11typedef long word_t;
12typedef struct { int fld1, fld2; } tcb_t;
13
14/**
15  DONT_TRANSLATE
16  */
17__attribute__((noreturn))
18static inline void
19fastpath_restore(word_t badge, word_t msgInfo, tcb_t *cur_thread)
20{
21    register word_t r0 asm ("r0") = badge;
22    register word_t r1 asm ("r1") = msgInfo;
23    asm volatile (
24            "add sp, %[cur_thread], %[offset]\n\t" /* Point to LR_svc */
25            "ldmdb sp, {r2-lr}^\n\t"
26            "rfeia sp\n\t"
27        :
28        : [offset] "i" (PT_LR_svc),
29          [cur_thread] "r" (cur_thread),
30          "r"(r0), "r"(r1)
31        : "memory" );
32}
33