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