1%
2% Copyright 2016, Data61, CSIRO
3%
4% This software may be distributed and modified according to the terms of
5% the GNU General Public License version 2. Note that NO WARRANTY is provided.
6% See "LICENSE_GPLv2.txt" for details.
7%
8% @TAG(DATA61_GPL)
9%
10
11This module defines the encoding of arch-specific faults.
12
13> module SEL4.API.Faults.X64 where
14
15\begin{impdetails}
16
17> import Prelude hiding (Word)
18> import SEL4.Machine
19> import SEL4.Model
20> import SEL4.Object.Structures
21> import SEL4.Object.TCB(asUser)
22
23\end{impdetails}
24
25> import SEL4.API.Failures.X64
26
27> makeArchFaultMessage :: ArchFault -> PPtr TCB -> Kernel (Word, [Word])
28> makeArchFaultMessage (VMFault vptr archData) thread = do
29>     pc <- asUser thread getRestartPC
30>     return (5, pc:fromVPtr vptr:archData)
31
32> handleArchFaultReply :: ArchFault -> PPtr TCB -> Word -> [Word] -> Kernel Bool
33> handleArchFaultReply (VMFault {}) _ _ _ = return True
34
35