1/* 2 * Copyright 2019, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 */ 6#include <stdio.h> 7#include <pb_encode.h> 8#include <pb_decode.h> 9#include <utils/fence.h> 10#include <sel4nanopb/sel4nanopb.h> 11#include <sel4/sel4.h> 12 13pb_ostream_t pb_ostream_from_IPC(seL4_Word offset) 14{ 15 char *msg_buffer = (char *) & (seL4_GetIPCBuffer()->msg[offset]); 16 size_t size = seL4_MsgMaxLength * sizeof(seL4_Word) - offset; 17 return pb_ostream_from_buffer(msg_buffer, size); 18} 19 20pb_istream_t pb_istream_from_IPC(seL4_Word offset) 21{ 22 char *msg_buffer = (char *) & (seL4_GetIPCBuffer()->msg[offset]); 23 size_t size = seL4_MsgMaxLength * sizeof(seL4_Word) - offset; 24 return pb_istream_from_buffer(msg_buffer, size); 25} 26