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