Index: kernel/arch/arm32/include/mach/integratorcp/integratorcp.h
===================================================================
--- kernel/arch/arm32/include/mach/integratorcp/integratorcp.h	(revision 5ac77cc96d78ca645a458a91b3c210a0a31dc894)
+++ kernel/arch/arm32/include/mach/integratorcp/integratorcp.h	(revision 851f33aff2fffc3d825f1b8b525fdf9ad2b9cb53)
@@ -36,6 +36,6 @@
  */
 
-#ifndef KERN_arm32_MACHINE_H_
-#define KERN_arm32_MACHINE_H_
+#ifndef KERN_arm32_icp_H_
+#define KERN_arm32_icp_H_
 
 #include <arch/machine_func.h>
@@ -106,4 +106,6 @@
 extern void icp_frame_init(void);
 
+extern struct arm_machine_ops icp_machine_ops;
+
 #endif
 
Index: kernel/arch/arm32/include/mach/testarm/testarm.h
===================================================================
--- kernel/arch/arm32/include/mach/testarm/testarm.h	(revision 5ac77cc96d78ca645a458a91b3c210a0a31dc894)
+++ kernel/arch/arm32/include/mach/testarm/testarm.h	(revision 851f33aff2fffc3d825f1b8b525fdf9ad2b9cb53)
@@ -37,6 +37,6 @@
  */
 
-#ifndef KERN_arm32_MACHINE_H_
-#define KERN_arm32_MACHINE_H_
+#ifndef KERN_arm32_testarm_H_
+#define KERN_arm32_testarm_H_
 
 #include <arch/machine_func.h>
@@ -76,4 +76,5 @@
 extern void gxemul_frame_init(void);
 
+extern struct arm_machine_ops gxemul_machine_ops;
 
 #endif
Index: kernel/arch/arm32/include/machine_func.h
===================================================================
--- kernel/arch/arm32/include/machine_func.h	(revision 5ac77cc96d78ca645a458a91b3c210a0a31dc894)
+++ kernel/arch/arm32/include/machine_func.h	(revision 851f33aff2fffc3d825f1b8b525fdf9ad2b9cb53)
@@ -57,6 +57,9 @@
 };
 
-extern struct arm_machine_ops machine_ops;
+/** Pointer to arm_machine_ops structure being used. */
+extern struct arm_machine_ops *machine_ops;
 
+/** Initialize machine_ops pointer. */
+extern void machine_ops_init(void);
 
 /** Maps HW devices to the kernel address space using #hw_map. */
Index: kernel/arch/arm32/src/arm32.c
===================================================================
--- kernel/arch/arm32/src/arm32.c	(revision 5ac77cc96d78ca645a458a91b3c210a0a31dc894)
+++ kernel/arch/arm32/src/arm32.c	(revision 851f33aff2fffc3d825f1b8b525fdf9ad2b9cb53)
@@ -63,4 +63,7 @@
 		    bootinfo->tasks[i].name);
 	}
+
+	/* Initialize machine_ops pointer. */
+	machine_ops_init();
 }
 
Index: kernel/arch/arm32/src/mach/integratorcp/integratorcp.c
===================================================================
--- kernel/arch/arm32/src/mach/integratorcp/integratorcp.c	(revision 5ac77cc96d78ca645a458a91b3c210a0a31dc894)
+++ kernel/arch/arm32/src/mach/integratorcp/integratorcp.c	(revision 851f33aff2fffc3d825f1b8b525fdf9ad2b9cb53)
@@ -56,5 +56,5 @@
 static icp_hw_map_t icp_hw_map;
 static irq_t icp_timer_irq;
-struct arm_machine_ops machine_ops = {
+struct arm_machine_ops icp_machine_ops = {
 	icp_init,
 	icp_timer_irq_start,
Index: kernel/arch/arm32/src/mach/testarm/testarm.c
===================================================================
--- kernel/arch/arm32/src/mach/testarm/testarm.c	(revision 5ac77cc96d78ca645a458a91b3c210a0a31dc894)
+++ kernel/arch/arm32/src/mach/testarm/testarm.c	(revision 851f33aff2fffc3d825f1b8b525fdf9ad2b9cb53)
@@ -56,5 +56,5 @@
 static irq_t gxemul_timer_irq;
 
-struct arm_machine_ops machine_ops = {
+struct arm_machine_ops gxemul_machine_ops = {
 	gxemul_init,
 	gxemul_timer_irq_start,
Index: kernel/arch/arm32/src/machine_func.c
===================================================================
--- kernel/arch/arm32/src/machine_func.c	(revision 5ac77cc96d78ca645a458a91b3c210a0a31dc894)
+++ kernel/arch/arm32/src/machine_func.c	(revision 851f33aff2fffc3d825f1b8b525fdf9ad2b9cb53)
@@ -39,10 +39,26 @@
 
 #include <arch/machine_func.h>
+#include <arch/mach/integratorcp/integratorcp.h>
+#include <arch/mach/testarm/testarm.h>
 
+/** Pointer to machine_ops structure being used. */
+struct arm_machine_ops *machine_ops;
+
+/** Initialize machine_ops pointer. */
+void machine_ops_init(void)
+{
+#if defined(MACHINE_testarm)
+	machine_ops = &gxemul_machine_ops;
+#elif defined(MACHINE_integratorcp)
+	machine_ops = &icp_machine_ops;
+#else
+#error Machine type not defined.
+#endif
+}
 
 /** Maps HW devices to the kernel address space using #hw_map. */
 void machine_init(void)
 {
-	(machine_ops.machine_init)();
+	(machine_ops->machine_init)();
 }
 
@@ -51,5 +67,5 @@
 void machine_timer_irq_start(void)
 {
-	(machine_ops.machine_timer_irq_start)();
+	(machine_ops->machine_timer_irq_start)();
 }
 
@@ -58,5 +74,5 @@
 void machine_cpu_halt(void)
 {
-	(machine_ops.machine_cpu_halt)();
+	(machine_ops->machine_cpu_halt)();
 }
 
@@ -68,5 +84,5 @@
 uintptr_t machine_get_memory_size(void)
 {
-	return (machine_ops.machine_get_memory_size)();
+	return (machine_ops->machine_get_memory_size)();
 }
 
@@ -78,5 +94,5 @@
 void machine_irq_exception(unsigned int exc_no, istate_t *istate)
 {
-	(machine_ops.machine_irq_exception)(exc_no, istate);
+	(machine_ops->machine_irq_exception)(exc_no, istate);
 }
 
@@ -87,5 +103,5 @@
 void machine_frame_init(void)
 {
-	(machine_ops.machine_frame_init)();
+	(machine_ops->machine_frame_init)();
 }
 
@@ -95,5 +111,5 @@
 void machine_output_init(void)
 {
-	(machine_ops.machine_output_init)();
+	(machine_ops->machine_output_init)();
 }
 
@@ -103,5 +119,5 @@
 void machine_input_init(void)
 {
-	(machine_ops.machine_input_init)();
+	(machine_ops->machine_input_init)();
 }