| /* | |
| * Copyright 2018, Data61, CSIRO (ABN 41 687 119 230) | |
| * | |
| * SPDX-License-Identifier: BSD-2-Clause | |
| */ | |
| #pragma once | |
| /* This file provides convenient wrappers around seL4 IPC buffer manipulation */ | |
| #include <autoconf.h> | |
| #include <sel4vka/gen_config.h> | |
| #include <vka/cspacepath_t.h> | |
| #include <vka/object.h> | |
| static inline void vka_set_cap_receive_path(const cspacepath_t *src) | |
| { | |
| seL4_SetCapReceivePath( | |
| /* _service */ src->root, | |
| /* index */ src->capPtr, | |
| /* depth */ src->capDepth | |
| ); | |
| } |