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