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#include <autoconf.h> 14 15base 64 16 17block VMFault { 18 padding 960 19 field IP 64 20 field Addr 64 21 field PrefetchFault 64 22 field FSR 64 23 padding 60 24 field seL4_FaultType 4 25} 26 27block NullFault { 28 padding 1216 29 padding 60 30 field seL4_FaultType 4 31} 32 33block CapFault { 34 padding 768 35 field IP 64 36 field Addr 64 37 field InRecvPhase 64 38 field LookupFailureType 64 39 -- these vary according to LookupFailureType 40 field MR4 64 41 field MR5 64 42 field MR6 64 43 padding 60 44 field seL4_FaultType 4 45} 46 47block UnknownSyscall { 48 field RAX 64 49 field RBX 64 50 field RCX 64 51 field RDX 64 52 field RSI 64 53 field RDI 64 54 field RBP 64 55 field R8 64 56 field R9 64 57 field R10 64 58 field R11 64 59 field R12 64 60 field R13 64 61 field R14 64 62 field R15 64 63 field FaultIP 64 64 field RSP 64 65 field FLAGS 64 66 field Syscall 64 67 padding 60 68 field seL4_FaultType 4 69} 70 71block UserException { 72 padding 896 73 field FaultIP 64 74 field Stack 64 75 field FLAGS 64 76 field Number 64 77 field Code 64 78 padding 60 79 field seL4_FaultType 4 80} 81 82#ifdef CONFIG_HARDWARE_DEBUG_API 83block DebugException { 84 padding 960 85 field FaultIP 64 86 field ExceptionReason 64 87 field TriggerAddress 64 88 field BreakpointNumber 64 89 padding 60 90 field seL4_FaultType 4 91} 92#endif 93 94block Timeout { 95 padding 1088 96 field data 64 97 field consumed 64 98 padding 60 99 field seL4_FaultType 4 100} 101 102#include <sel4/arch/shared_types.bf> 103