1(*
2 * Copyright 2014, General Dynamics C4 Systems
3 *
4 * SPDX-License-Identifier: GPL-2.0-only
5 *)
6
7(*
8Formalisation of interrupt handling.
9*)
10
11chapter "Arch-specific Interrupts"
12
13theory ArchInterrupt_A
14imports Ipc_A
15begin
16
17context Arch begin global_naming ARM_A
18
19definition handle_reserved_irq :: "irq \<Rightarrow> (unit,'z::state_ext) s_monad"
20  where "handle_reserved_irq irq = return ()"
21
22fun arch_invoke_irq_handler :: "irq_handler_invocation \<Rightarrow> (unit,'z::state_ext) s_monad"
23  where
24  "arch_invoke_irq_handler (ACKIrq irq) = (do_machine_op $ maskInterrupt False irq)"
25| "arch_invoke_irq_handler _ = return ()"
26
27definition arch_mask_irq_signal :: "irq \<Rightarrow> (unit,'z::state_ext) s_monad"
28  where
29  "arch_mask_irq_signal irq \<equiv> do_machine_op $ maskInterrupt True irq"
30
31end
32
33end
34