| /* |
| * Copyright 2017, Data61 |
| * Commonwealth Scientific and Industrial Research Organisation (CSIRO) |
| * ABN 41 687 119 230. |
| * |
| * This software may be distributed and modified according to the terms of |
| * the BSD 2-Clause license. Note that NO WARRANTY is provided. |
| * See "LICENSE_BSD2.txt" for details. |
| * |
| * @TAG(DATA61_BSD) |
| */ |
| |
| #pragma once |
| |
| #include <allocman/allocman.h> |
| #include <allocman/cspace/cspace.h> |
| #include <vka/capops.h> |
| |
| /* Helper routines for treating cspaces in a high level way. Giving you seL4 like operations |
| * at the cspace level instead of the cap/slot level */ |
| |
| static inline int cspace_move_alloc(allocman_t *alloc, cspacepath_t src, cspacepath_t *result) { |
| int error; |
| error = allocman_cspace_alloc(alloc, result); |
| if (error) { |
| return error; |
| } |
| return vka_cnode_move(result, &src) != seL4_NoError; |
| } |
| |
| static inline int cspace_move_alloc_cptr(allocman_t *alloc, cspace_interface_t source_cspace, seL4_CPtr slot, cspacepath_t *result) { |
| return cspace_move_alloc(alloc, source_cspace.make_path(source_cspace.cspace, slot), result); |
| } |
| |