Index: kernel/arch/arm32/include/cp15.h
===================================================================
--- kernel/arch/arm32/include/cp15.h	(revision 467f0c015bfe6def2a857f40db3faa9f3379815f)
+++ kernel/arch/arm32/include/cp15.h	(revision 1f271d9d0a71b80c48d28c265407007ab0a07331)
@@ -45,5 +45,5 @@
 { \
 	uint32_t val; \
-	asm volatile ( "mrc p15, opc1, %0, crn, crm, opc2\n" : "=r" (val) ); \
+	asm volatile ( "mrc p15, "#opc1", %0, "#crn", "#crm", "#opc2"\n" : "=r" (val) ); \
 	return val; \
 }
@@ -51,5 +51,5 @@
 static inline void name##_write(uint32_t val) \
 { \
-	asm volatile ( "mrc p15, opc1, %0, crn, crm, opc2\n" :: "r" (val) ); \
+	asm volatile ( "mrc p15, "#opc1", %0, "#crn", "#crm", "#opc2"\n" :: "r" (val) ); \
 }