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