| /* | |
| * Copyright 2017, Data61, CSIRO (ABN 41 687 119 230) | |
| * | |
| * SPDX-License-Identifier: BSD-2-Clause | |
| */ | |
| #pragma once | |
| #include <sel4/types.h> | |
| #include <allocman/properties.h> | |
| #include <vka/cspacepath_t.h> | |
| struct allocman; | |
| typedef struct cspace_interface { | |
| int (*alloc)(struct allocman *alloc, void *cookie, cspacepath_t *path); | |
| void (*free)(struct allocman *alloc, void *cookie, const cspacepath_t *path); | |
| cspacepath_t (*make_path)(void *cookie, seL4_CPtr slot); | |
| struct allocman_properties properties; | |
| void *cspace; | |
| } cspace_interface_t; | |