1(*
2 * Copyright 2014, General Dynamics C4 Systems
3 *
4 * SPDX-License-Identifier: GPL-2.0-only
5 *)
6
7(*
8Functions for fault handling.
9*)
10
11chapter \<open>arch fault related functions\<close>
12
13theory ArchFault_A
14imports Structures_A Tcb_A
15begin
16
17context Arch begin global_naming ARM_A
18
19fun make_arch_fault_msg :: "arch_fault \<Rightarrow> obj_ref \<Rightarrow> (data \<times> data list,'z::state_ext) s_monad"
20where
21 "make_arch_fault_msg (VMFault vptr archData) thread = do
22     pc \<leftarrow> as_user thread getRestartPC;
23     return (5, pc # vptr # archData) od"
24
25definition
26  handle_arch_fault_reply :: "arch_fault \<Rightarrow> obj_ref \<Rightarrow> data \<Rightarrow> data list \<Rightarrow> (bool,'z::state_ext) s_monad"
27where
28  "handle_arch_fault_reply vmf thread x y \<equiv> return True"
29
30
31end
32
33end
34