1-- 2-- Copyright 2017, Data61 3-- Commonwealth Scientific and Industrial Research Organisation (CSIRO) 4-- ABN 41 687 119 230. 5-- 6-- This software may be distributed and modified according to the terms of 7-- the BSD 2-Clause license. Note that NO WARRANTY is provided. 8-- See "LICENSE_BSD2.txt" for details. 9-- 10-- @TAG(DATA61_BSD) 11-- 12 13-- this file contains types shared between libsel4 and the kernel 14 15tagged_union seL4_Fault seL4_FaultType { 16 -- generic faults 17 tag NullFault 0 18 tag CapFault 1 19 tag UnknownSyscall 2 20 tag UserException 3 21#ifdef CONFIG_HARDWARE_DEBUG_API 22 tag DebugException 4 23#endif 24 tag Timeout 5 25 26 -- arch specific faults 27 tag VMFault 6 28 29#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT 30 tag VGICMaintenance 7 31 tag VCPUFault 8 32#endif 33} 34