1/*
2 * Copyright 2014, General Dynamics C4 Systems
3 *
4 * SPDX-License-Identifier: GPL-2.0-only
5 */
6
7#pragma once
8
9#include <mode/fastpath/fastpath.h>
10
11#ifndef CONFIG_KERNEL_MCS
12static inline int fastpath_reply_cap_check(cap_t cap)
13{
14    return cap_capType_equals(cap, cap_reply_cap);
15}
16#endif
17
18void slowpath(syscall_t syscall)
19NORETURN;
20
21void fastpath_call(word_t cptr, word_t r_msgInfo)
22NORETURN;
23
24#ifdef CONFIG_KERNEL_MCS
25void fastpath_reply_recv(word_t cptr, word_t r_msgInfo, word_t reply)
26#else
27void fastpath_reply_recv(word_t cptr, word_t r_msgInfo)
28#endif
29NORETURN;
30