Index: kernel/genarch/include/genarch/drivers/bcm2835/irc.h
===================================================================
--- kernel/genarch/include/genarch/drivers/bcm2835/irc.h	(revision 8be323084b791c62927f9cbb14696265246370dd)
+++ kernel/genarch/include/genarch/drivers/bcm2835/irc.h	(revision 3ede4402c7e2d73cb84f9c62c9e9207062cf813c)
@@ -1,3 +1,4 @@
 /*
+ * Copyright (c) 2019 Jiri Svoboda
  * Copyright (c) 2012 Jan Vesely
  * Copyright (c) 2013 Beniamino Galvani
@@ -59,6 +60,4 @@
 #define IRQ_PEND_SHORT_S	10
 
-unsigned shortcut_inums[] = { 7, 9, 10, 18, 19, 53, 54, 55, 56, 57, 62 };
-
 typedef struct {
 	ioport32_t	irq_basic_pending;
@@ -75,98 +74,8 @@
 #define BCM2835_IRQ_COUNT 96
 
-static inline void bcm2835_irc_dump(bcm2835_irc_t *regs)
-{
-#define DUMP_REG(name) \
-	printf("%s : %08x\n", #name, regs->name);
-
-	DUMP_REG(irq_basic_pending);
-	DUMP_REG(irq_pending1);
-	DUMP_REG(irq_pending2);
-	DUMP_REG(fiq_control);
-
-	for (int i = 0; i < 3; ++i) {
-		DUMP_REG(irq_enable[i]);
-		DUMP_REG(irq_disable[i]);
-	}
-#undef DUMP_REG
-}
-
-static inline void bcm2835_irc_init(bcm2835_irc_t *regs)
-{
-	/* Disable all interrupts */
-	regs->irq_disable[BANK_GPU0] = 0xffffffff;
-	regs->irq_disable[BANK_GPU1] = 0xffffffff;
-	regs->irq_disable[BANK_ARM]  = 0xffffffff;
-
-	/* Disable FIQ generation */
-	regs->fiq_control = 0;
-}
-
-static inline int ffs(unsigned int x)
-{
-	int ret;
-
-	asm volatile (
-	    "clz r0, %[x]\n"
-	    "rsb %[ret], r0, #32\n"
-	    : [ret] "=r" (ret)
-	    : [x] "r" (x)
-	    : "r0"
-	);
-
-	return ret;
-}
-
-static inline unsigned bcm2835_irc_inum_get(bcm2835_irc_t *regs)
-{
-	uint32_t pending;
-	int inum = -1;
-
-	pending = regs->irq_basic_pending;
-
-	/*
-	 * The basic pending register shows interrupts pending from ARM
-	 * peripherals and it also contains, in order to speed up processing,
-	 * additional information about pending GPU interrupts:
-	 *
-	 *  - bits 0-7 are associated to ARM peripherals
-	 *  - bit 8 is 1 when at least one bit is set in pending register 1
-	 *  - bit 9 is 1 when at least one bit is set in pending register 2
-	 *  - bits 10-20 indicate pending status of selected GPU peripherals
-	 *
-	 *  Reference: BCM2835 ARM Peripherals, p.113
-	 */
-
-	if (pending & IRQ_PEND_ARM_M) {
-		inum = MAKE_IRQ(BANK_ARM, ffs(pending & IRQ_PEND_ARM_M) - 1);
-	} else if (pending & IRQ_PEND_SHORT_M) {
-		int pos = (pending & IRQ_PEND_SHORT_M) >> IRQ_PEND_SHORT_S;
-		inum = shortcut_inums[ffs(pos) - 1];
-	} else if (pending & IRQ_PEND_GPU0_M) {
-		inum = MAKE_IRQ(BANK_GPU0, ffs(regs->irq_pending1) - 1);
-	} else if (pending & IRQ_PEND_GPU1_M) {
-		inum = MAKE_IRQ(BANK_GPU1, ffs(regs->irq_pending2) - 1);
-	}
-
-	if (inum < 0) {
-		printf("Spurious interrupt!\n");
-		bcm2835_irc_dump(regs);
-		inum = 0;
-	}
-
-	return inum;
-}
-
-static inline void bcm2835_irc_enable(bcm2835_irc_t *regs, unsigned inum)
-{
-	assert(inum < BCM2835_IRQ_COUNT);
-	regs->irq_enable[IRQ_TO_BANK(inum)] |= (1 << IRQ_TO_NUM(inum));
-}
-
-static inline void bcm2835_irc_disable(bcm2835_irc_t *regs, unsigned inum)
-{
-	assert(inum < BCM2835_IRQ_COUNT);
-	regs->irq_disable[IRQ_TO_BANK(inum)] |= (1 << IRQ_TO_NUM(inum));
-}
+extern void bcm2835_irc_init(bcm2835_irc_t *);
+extern unsigned bcm2835_irc_inum_get(bcm2835_irc_t *);
+extern void bcm2835_irc_enable(bcm2835_irc_t *, unsigned);
+extern void bcm2835_irc_disable(bcm2835_irc_t *, unsigned);
 
 #endif /* KERN_BCM2835_IRQC_H_ */
Index: kernel/genarch/include/genarch/drivers/bcm2835/mbox.h
===================================================================
--- kernel/genarch/include/genarch/drivers/bcm2835/mbox.h	(revision 8be323084b791c62927f9cbb14696265246370dd)
+++ kernel/genarch/include/genarch/drivers/bcm2835/mbox.h	(revision 3ede4402c7e2d73cb84f9c62c9e9207062cf813c)
@@ -134,8 +134,9 @@
 } bcm2835_fb_desc_t;
 
-bool bcm2835_prop_get_memory(uint32_t *base, uint32_t *size);
-bool bcm2835_fb_init(fb_properties_t *prop);
+extern bool bcm2835_prop_get_memory(uint32_t *base, uint32_t *size);
+extern bool bcm2835_fb_init(fb_properties_t *prop);
 
 #endif
+
 /**
  * @}
Index: kernel/genarch/include/genarch/drivers/bcm2835/timer.h
===================================================================
--- kernel/genarch/include/genarch/drivers/bcm2835/timer.h	(revision 8be323084b791c62927f9cbb14696265246370dd)
+++ kernel/genarch/include/genarch/drivers/bcm2835/timer.h	(revision 3ede4402c7e2d73cb84f9c62c9e9207062cf813c)
@@ -64,21 +64,10 @@
 } bcm2835_timer_t;
 
-static inline void bcm2835_timer_start(bcm2835_timer_t *timer)
-{
-	assert(timer);
-	/* Clear pending interrupt on channel 1 */
-	timer->cs |= BCM2835_TIMER_CS_M1;
-	/* Initialize compare value for match channel 1 */
-	timer->c1 = timer->clo + (BCM2835_CLOCK_FREQ / HZ);
-}
-
-static inline void bcm2835_timer_irq_ack(bcm2835_timer_t *timer)
-{
-	assert(timer);
-	/* Clear pending interrupt on channel 1 */
-	timer->cs |= BCM2835_TIMER_CS_M1;
-	/* Reprogram compare value for match channel 1 */
-	timer->c1 = timer->clo + (BCM2835_CLOCK_FREQ / HZ);
-}
+extern void bcm2835_timer_start(bcm2835_timer_t *);
+extern void bcm2835_timer_irq_ack(bcm2835_timer_t *);
 
 #endif /* KERN_BCM2835_TIMER_H_ */
+
+/**
+ * @}
+ */