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