1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: GPL-2.0-only
5 *)
6
7(*
8Arch Functions for cancelling IPC.
9*)
10
11chapter \<open>Arch IPC Cancelling\<close>
12
13theory ArchIpcCancel_A
14imports CSpaceAcc_A
15begin
16
17context Arch begin global_naming ARM_A
18
19text \<open>Actions to be taken after a cap is deleted\<close>
20definition
21  arch_post_cap_deletion :: "arch_cap \<Rightarrow> (unit, 'z::state_ext) s_monad"
22where
23  "arch_post_cap_deletion _ \<equiv> return ()"
24
25text \<open>Arch specific generic object references not covered by generic references\<close>
26datatype arch_gen_obj_ref = unit
27
28definition
29  arch_gen_obj_refs :: "arch_cap \<Rightarrow> arch_gen_obj_ref set"
30where
31  "arch_gen_obj_refs _ = {}"
32
33definition
34  arch_cap_cleanup_opt :: "arch_cap \<Rightarrow> cap"
35where
36  "arch_cap_cleanup_opt ac \<equiv> NullCap"
37
38end
39end
40