1--
2-- Copyright 2016, 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--
14-- Copyright 2016, 2017 Hesham Almatary, Data61/CSIRO <hesham.almatary@data61.csiro.au>
15-- Copyright 2015, 2016 Hesham Almatary <heshamelmatary@gmail.com>
16
17#include <autoconf.h>
18
19base 64
20
21---- Arch-independent object types
22
23block VMFault {
24    padding   512
25    field     IP                64
26    field     Addr              64
27    field     PrefetchFault     64
28    padding                     32
29    field     FSR               5
30    padding                     8
31    padding                     16
32    field     seL4_FaultType    3
33}
34
35-- VM attributes
36block vm_attributes {
37    padding 32
38    padding 31
39    field riscvExecuteNever  1
40}
41
42block NullFault {
43   padding 704
44   padding 61
45   field seL4_FaultType 3
46}
47
48block CapFault {
49   padding 256
50   field IP   64
51   field Addr 64
52   field InRecvPhase 64
53   field LookupFailureType 64
54   -- these vary according to LookupFailureType
55   field MR4 64
56   field MR5 64
57   field MR6 64
58   padding 61
59   field seL4_FaultType 3
60}
61
62block UnknownSyscall {
63   field FaultIP 64
64   field SP 64
65   field RA 64
66   field A0 64
67   field A1 64
68   field A2 64
69   field A3 64
70   field A4 64
71   field A5 64
72   field A6 64
73   field Syscall 64
74   padding 61
75   field seL4_FaultType 3
76}
77
78block UserException {
79   padding 384
80   field FaultIP 64
81   field SP      64
82   field FLAGS   64
83   field Number  64
84   field Code    64
85   padding 61
86   field seL4_FaultType 3
87}
88
89#include <sel4/arch/shared_types.bf>
90