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