Index: kernel/arch/arm32/src/mach/beagleboardxm/beagleboardxm.c
===================================================================
--- kernel/arch/arm32/src/mach/beagleboardxm/beagleboardxm.c	(revision d701672cfbc89b61a58acf8b6c2ffa3b53e13fe6)
+++ kernel/arch/arm32/src/mach/beagleboardxm/beagleboardxm.c	(revision b76ce3fafabca2ee4bc41e417ad02ab3546c67f2)
@@ -35,4 +35,5 @@
 #include <arch/exception.h>
 #include <arch/mach/beagleboardxm/beagleboardxm.h>
+#include <assert.h>
 #include <genarch/drivers/amdm37x/uart.h>
 #include <genarch/drivers/amdm37x/irc.h>
@@ -102,5 +103,5 @@
 	    (void *) km_map(AMDM37x_IRC_BASE_ADDRESS, AMDM37x_IRC_SIZE,
 	    PAGE_NOT_CACHEABLE);
-	ASSERT(beagleboard.irc_addr);
+	assert(beagleboard.irc_addr);
 	omap_irc_init(beagleboard.irc_addr);
 
Index: kernel/arch/arm32/src/mach/beaglebone/beaglebone.c
===================================================================
--- kernel/arch/arm32/src/mach/beaglebone/beaglebone.c	(revision d701672cfbc89b61a58acf8b6c2ffa3b53e13fe6)
+++ kernel/arch/arm32/src/mach/beaglebone/beaglebone.c	(revision b76ce3fafabca2ee4bc41e417ad02ab3546c67f2)
@@ -36,4 +36,5 @@
 #include <arch/exception.h>
 #include <arch/mach/beaglebone/beaglebone.h>
+#include <assert.h>
 #include <genarch/drivers/am335x/irc.h>
 #include <genarch/drivers/am335x/uart.h>
@@ -98,8 +99,8 @@
 	    AM335x_CTRL_MODULE_SIZE, PAGE_NOT_CACHEABLE);
 
-	ASSERT(bbone.irc_addr != NULL);
-	ASSERT(bbone.cm_per_addr != NULL);
-	ASSERT(bbone.cm_dpll_addr != NULL);
-	ASSERT(bbone.ctrl_module != NULL);
+	assert(bbone.irc_addr != NULL);
+	assert(bbone.cm_per_addr != NULL);
+	assert(bbone.cm_dpll_addr != NULL);
+	assert(bbone.ctrl_module != NULL);
 
 	/* Initialize the interrupt controller */
Index: kernel/arch/arm32/src/mach/raspberrypi/raspberrypi.c
===================================================================
--- kernel/arch/arm32/src/mach/raspberrypi/raspberrypi.c	(revision d701672cfbc89b61a58acf8b6c2ffa3b53e13fe6)
+++ kernel/arch/arm32/src/mach/raspberrypi/raspberrypi.c	(revision b76ce3fafabca2ee4bc41e417ad02ab3546c67f2)
@@ -36,4 +36,5 @@
 #include <arch/exception.h>
 #include <arch/mach/raspberrypi/raspberrypi.h>
+#include <assert.h>
 #include <genarch/drivers/pl011/pl011.h>
 #include <genarch/drivers/bcm2835/irc.h>
@@ -103,5 +104,5 @@
 	raspi.irc = (void *) km_map(BCM2835_IRC_ADDR, sizeof(bcm2835_irc_t),
 				    PAGE_NOT_CACHEABLE);
-	ASSERT(raspi.irc);
+	assert(raspi.irc);
 	bcm2835_irc_init(raspi.irc);