Index: kernel/genarch/include/genarch/drivers/bcm2835/mbox.h
===================================================================
--- kernel/genarch/include/genarch/drivers/bcm2835/mbox.h	(revision f22f679fa78e8a86ddf97362ae98660cdb16ee13)
+++ kernel/genarch/include/genarch/drivers/bcm2835/mbox.h	(revision 44186b01d3b878161e7f5317266c5bc425c4b2a6)
@@ -84,7 +84,7 @@
 #define MBOX_ADDR_ALIGN		16
 
-#define ALLOC_PROP_BUFFER(name,type)					\
-	char _tmp[sizeof(type) + MBOX_ADDR_ALIGN] = { 0 };		\
-	type *name = (type *)ALIGN_UP((uint32_t)_tmp, MBOX_ADDR_ALIGN);
+#define MBOX_BUFF_ALLOC(name, type)					\
+	char tmp_ ## name[sizeof(type) + MBOX_ADDR_ALIGN] = { 0 };      \
+	type *name = (type *)ALIGN_UP((uintptr_t)tmp_ ## name, MBOX_ADDR_ALIGN);
 
 typedef struct {
Index: kernel/genarch/src/drivers/bcm2835/mbox.c
===================================================================
--- kernel/genarch/src/drivers/bcm2835/mbox.c	(revision f22f679fa78e8a86ddf97362ae98660cdb16ee13)
+++ kernel/genarch/src/drivers/bcm2835/mbox.c	(revision 44186b01d3b878161e7f5317266c5bc425c4b2a6)
@@ -35,5 +35,4 @@
 
 #include <mm/km.h>
-#include <mm/slab.h>
 #include <typedefs.h>
 #include <genarch/drivers/bcm2835/mbox.h>
@@ -60,5 +59,5 @@
 {
 	bool ret;
-	ALLOC_PROP_BUFFER(req, mbox_getmem_buf_t);
+	MBOX_BUFF_ALLOC(req, mbox_getmem_buf_t);
 
 	req->buf_hdr.size = sizeof(mbox_getmem_buf_t);
@@ -88,16 +87,9 @@
 {
 	bcm2835_mbox_t *fb_mbox;
-	bcm2835_fb_desc_t *fb_desc;
-	void *fb_desc_buf;
 	bool ret = false;
-
-	fb_desc_buf = malloc(sizeof(bcm2835_fb_desc_t) + MBOX_ADDR_ALIGN, 0);
-	if (!fb_desc_buf)
-		return false;
+        MBOX_BUFF_ALLOC(fb_desc, bcm2835_fb_desc_t);
 
 	fb_mbox = (void *) km_map(BCM2835_MBOX0_ADDR, sizeof(bcm2835_mbox_t),
 				  PAGE_NOT_CACHEABLE);
-	fb_desc = (bcm2835_fb_desc_t *) ALIGN_UP((uintptr_t)fb_desc_buf,
-						 MBOX_ADDR_ALIGN);
 
 	fb_desc->width = 640;
@@ -131,5 +123,4 @@
 out:
 	km_unmap((uintptr_t)fb_mbox, sizeof(bcm2835_mbox_t));
-	free(fb_desc_buf);
 	return ret;
 }