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 <linker.h>
10#include <mode/fastpath/fastpath.h>
11#include <benchmark/benchmark_track.h>
12#include <arch/machine/debug.h>
13
14void slowpath(syscall_t syscall)
15NORETURN;
16
17static inline
18void fastpath_call(word_t cptr, word_t r_msgInfo)
19NORETURN;
20
21static inline
22#ifdef CONFIG_KERNEL_MCS
23void fastpath_reply_recv(word_t cptr, word_t r_msgInfo, word_t reply)
24#else
25void fastpath_reply_recv(word_t cptr, word_t r_msgInfo)
26#endif
27NORETURN;
28
29
30