1/*#
2 *#Copyright 2017, 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/*- set client_ids = namespace() -*/
14/*- if me.parent.type.to_threads == 0 -*/
15    /*- include 'seL4RPCNoThreads-to.template.c' -*/
16    /*- from 'global-endpoint.template.c' import allocate_rpc_endpoint_cap with context -*/
17    /*- do allocate_rpc_endpoint_cap(me.parent.to_end, is_reader=True, other_end=me.parent.from_ends[0]) -*/
18    /*- set client_ids.badges = pop('badges') -*/
19
20/*- else -*/
21    /*- include 'seL4RPCCall-to.template.c' -*/
22    /*- from 'rpc-connector.c' import allocate_badges with context -*/
23    /*- do allocate_badges(client_ids) -*/
24/*- endif -*/
25/*- include 'seL4MultiSharedData-to.template.c' -*/
26