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 sel4arch specific 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_KERNEL_MCS
16    tag Timeout 5
17
18    -- arch specific faults
19    tag VMFault 6
20#else
21    -- arch specific faults
22    tag VMFault 5
23#endif
24}
25