1/* 2 * Copyright 2019, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: BSD-2-Clause 5 */ 6 7#include <sel4vm/guest_vm.h> 8 9struct vgic_dist_device { 10 uintptr_t pstart; 11 size_t size; 12 void *priv; 13}; 14 15const struct vgic_dist_device dev_vgic_dist; 16 17int vm_install_vgic(vm_t *vm); 18int vm_vgic_maintenance_handler(vm_vcpu_t *vcpu); 19