1 /*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 */
6
7 #pragma once
8 #include <autoconf.h>
9 #include <sel4/types.h>
10 #include <sel4/macros.h>
11 #include <sel4/invocation.h>
12 #include <sel4/constants.h>
13 #include <interfaces/sel4_client.h>
14
15 /*
16 * This file specifies virtual implementations of older invocations
17 * that can be aliased directly to new invocations.
18 */
19
20 #ifdef CONFIG_KERNEL_MCS
seL4_SchedControl_Configure(seL4_SchedControl _service,seL4_SchedContext schedcontext,seL4_Time budget,seL4_Time period,seL4_Word extra_refills,seL4_Word badge)21 LIBSEL4_INLINE seL4_Error seL4_SchedControl_Configure(seL4_SchedControl _service, seL4_SchedContext schedcontext,
22 seL4_Time budget, seL4_Time period, seL4_Word extra_refills, seL4_Word badge)
23 {
24 return seL4_SchedControl_ConfigureFlags(_service, schedcontext, budget, period, extra_refills, badge,
25 seL4_SchedContext_NoFlag);
26 }
27 #endif
28