| /* |
| * Copyright 2020, Data61, ABN 41 687 119 230. |
| * |
| * SPDX-License-Identifier: BSD-2-Clause |
| */ |
| |
| /*- from 'rpc-connector.c' import establish_from_rpc, begin_send, perform_call, release_recv with context -*/ |
| /*- from 'global-endpoint.template.c' import allocate_rpc_endpoint_cap with context -*/ |
| #include <camkes/dataport.h> |
| |
| /*? macros.show_includes(me.instance.type.includes) ?*/ |
| /*? macros.show_includes(me.interface.type.includes) ?*/ |
| |
| /*- set connector = namespace() -*/ |
| |
| /*- set connector.language = 'c' -*/ |
| /*# Establish the buffer for message contents #*/ |
| /*- set connector.userspace_ipc = False -*/ |
| /*- set base = '((void*)&seL4_GetIPCBuffer()->msg[0])' -*/ |
| /*- set buffer_size = '(seL4_MsgMaxLength * sizeof(seL4_Word))' -*/ |
| /*- set connector.lock = False -*/ |
| /*- set connector.send_buffer = base -*/ |
| /*- set connector.recv_buffer = base -*/ |
| /*- set connector.send_buffer_size = buffer_size -*/ |
| /*- set connector.recv_buffer_size = buffer_size -*/ |
| /*- set connector.recv_buffer_size_fixed = connector.userspace_ipc -*/ |
| |
| /*# Ensure the endpoint is allocated #*/ |
| /*- do allocate_rpc_endpoint_cap(me.parent.to_end, is_reader=False, other_end=me) -*/ |
| /*- set connector.badges = pop('badges') -*/ |
| /*- set connector.ep = pop('endpoint') -*/ |
| |
| |
| /*- include 'rpc-connector-common-from.c' -*/ |
