1/*
2 * Copyright 2014, General Dynamics C4 Systems
3 *
4 * SPDX-License-Identifier: GPL-2.0-only
5 */
6
7#pragma once
8
9#include <types.h>
10#include <api/failures.h>
11#include <object/structures.h>
12
13static inline void handleReservedIRQ(irq_t irq)
14{
15#ifdef CONFIG_IRQ_REPORTING
16    printf("Received unhandled reserved IRQ: %d\n", (int)irq);
17#endif
18}
19
20exception_t Arch_decodeIRQControlInvocation(word_t invLabel, word_t length,
21                                            cte_t *srcSlot, extra_caps_t excaps,
22                                            word_t *buffer);
23exception_t Arch_checkIRQ(word_t irq_w);
24
25