1/*
2 * Copyright 2020, Data61
3 * Commonwealth Scientific and Industrial Research Organisation (CSIRO)
4 * ABN 41 687 119 230.
5 *
6 * This software may be distributed and modified according to the terms of
7 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
8 * See "LICENSE_BSD2.txt" for details.
9 *
10 * @TAG(DATA61_BSD)
11 */
12
13
14/*- from 'rpc-connector.c' import establish_recv_rpc, recv_first_rpc, complete_recv, begin_recv, begin_reply, complete_reply, reply_recv with context -*/
15/*- from 'global-endpoint.template.c' import allocate_rpc_endpoint_cap with context -*/
16
17/*# Ensure the endpoint is allocated #*/
18/*- do allocate_rpc_endpoint_cap(me, is_reader=True, other_end=me.parent.from_ends[0]) -*/
19/*- set badges = pop('badges') -*/
20/*- set ep = pop('endpoint') -*/
21
22#define /*? me.interface.name ?*/_num_clients() /*? len(badges) ?*/
23
24#define /*? me.interface.name ?*/_BADGES_MACRO_X_ITERATOR() \
25/*- for b in badges --*/
26	X(/*?b?*/) \
27/*- endfor -*/
28
29int /*? me.interface.name ?*/_handle_message(seL4_MessageInfo_t *info, seL4_Word badge);
30