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