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