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 11chapter "Handle Hyperviser Fault Event" 12 13theory Hypervisor_A 14imports "../Exceptions_A" 15begin 16 17context Arch begin global_naming X64_A 18 19fun handle_hypervisor_fault :: "machine_word \<Rightarrow> hyp_fault_type \<Rightarrow> (unit, 'z::state_ext) s_monad" 20where 21"handle_hypervisor_fault thread X64NoHypFaults = return ()" 22 23 24end 25end 26