| /* |
| * Copyright 2018, Data61, CSIRO (ABN 41 687 119 230) |
| * |
| * SPDX-License-Identifier: BSD-2-Clause |
| */ |
| |
| #include <sel4/sel4.h> |
| #include <utils/util.h> |
| |
| {% raw %} |
| #define DECLARE_IPCBUFFER_SYMBOL(symbol) \ |
| extern char symbol[]; \ |
| void CONSTRUCTOR(199) setIPCBuffer(void) { \ |
| __sel4_ipc_buffer = (seL4_IPCBuffer *) symbol;\ |
| } |
| {% endraw %} |
| |
| DECLARE_IPCBUFFER_SYMBOL({{ipc_buffer_symbol}}) |
| |
| #define SIZED_SYMBOL(symbol, size, section) \ |
| char symbol[size] VISIBLE ALIGN(4096) SECTION(section); |
| |
| {% for (symbol, slot) in slots -%} |
| seL4_CPtr {{symbol}} = {{slot}}; |
| {% endfor %} |
| |
| {% for (symbol, size, section) in symbols -%} |
| SIZED_SYMBOL({{symbol}}, {{size}}, "{{section}}") |
| {% endfor %} |
| |
| |
| char progname[] = "{{progname}}"; |
