1--
2-- Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3-- Copyright 2015, 2016 Hesham Almatary <heshamelmatary@gmail.com>
4--
5-- SPDX-License-Identifier: BSD-2-Clause
6--
7
8#include <autoconf.h>
9
10base 32
11
12---- Arch-independent object types
13
14block VMFault {
15    padding   256
16    field     IP                32
17    field     Addr              32
18    field     PrefetchFault     32
19    field     FSR               5
20    padding                     8
21    padding                     15
22    field     seL4_FaultType    4
23}
24
25-- VM attributes
26block vm_attributes {
27    padding 31
28    field riscvExecuteNever  1
29}
30
31block NullFault {
32   padding 352
33   padding 28
34   field seL4_FaultType 4
35}
36
37block CapFault {
38   padding 128
39   field IP   32
40   field Addr 32
41   field InRecvPhase 32
42   field LookupFailureType 32
43   -- these vary according to LookupFailureType
44   field MR4 32
45   field MR5 32
46   field MR6 32
47   padding 28
48   field seL4_FaultType 4
49}
50
51block UnknownSyscall {
52   field FaultIP 32
53   field SP 32
54   field RA 32
55   field A0 32
56   field A1 32
57   field A2 32
58   field A3 32
59   field A4 32
60   field A5 32
61   field A6 32
62   field Syscall 32
63   padding 28
64   field seL4_FaultType 4
65}
66
67block UserException {
68   padding 224
69   field FaultIP 32
70   field SP      32
71   field Number  32
72   field Code    32
73   padding 28
74   field seL4_FaultType 4
75}
76
77#ifdef CONFIG_KERNEL_MCS
78block Timeout {
79    padding 256
80    field data 32
81    field consumed_high 32
82    field consumed_low 32
83    padding 28
84    field seL4_FaultType 4
85}
86#endif
87
88#include <sel4/arch/shared_types.bf>
89