1-- 2-- Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3-- 4-- SPDX-License-Identifier: BSD-2-Clause 5-- 6 7-- this file contains types shared between libsel4 and the kernel 8 9tagged_union seL4_Fault seL4_FaultType { 10 -- generic faults 11 tag NullFault 0 12 tag CapFault 1 13 tag UnknownSyscall 2 14 tag UserException 3 15#ifdef CONFIG_HARDWARE_DEBUG_API 16 tag DebugException 4 17#endif 18#ifdef CONFIG_KERNEL_MCS 19 tag Timeout 5 20 21 -- arch specific faults 22 tag VMFault 6 23 24#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT 25 tag VGICMaintenance 7 26 tag VCPUFault 8 27 tag VPPIEvent 9 28#endif 29#else 30 -- arch specific faults 31 tag VMFault 5 32 33#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT 34 tag VGICMaintenance 6 35 tag VCPUFault 7 36 tag VPPIEvent 8 37#endif 38#endif 39 40} 41