1/*
2 * Copyright 2019, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 */
6
7#include <sel4/sel4.h>
8#include <vka/object.h>
9#include <vka/capops.h>
10
11#include <sel4vm/guest_vm.h>
12#include <sel4vmmplatsupport/arch/service.h>
13
14int vmm_install_service(vm_t *vm, seL4_CPtr service, int index, uint32_t b)
15{
16    cspacepath_t src, dst;
17    seL4_Word badge = b;
18    int err;
19    vka_cspace_make_path(vm->vka, service, &src);
20    dst.root = vm->cspace.cspace_obj.cptr;
21    dst.capPtr = index;
22    dst.capDepth = VM_CSPACE_SIZE_BITS;
23    err =  vka_cnode_mint(&dst, &src, seL4_AllRights, badge);
24    return err;
25}
26
27
28