diff --git a/include/arch/arm/arch/object/vcpu.h b/include/arch/arm/arch/object/vcpu.h
index b26b9a462..014d69975 100644
--- a/include/arch/arm/arch/object/vcpu.h
+++ b/include/arch/arm/arch/object/vcpu.h
@@ -74,8 +74,8 @@ exception_t invokeVCPUSetTCB(vcpu_t *vcpu, tcb_t *tcb);
 #else /* end of CONFIG_ARM_HYPERVISOR_SUPPORT */
 
 /* used in boot.c with a guard, use a marco to avoid exposing vcpu_t */
-#define vcpu_restore(x)
-#define vcpu_switch(x)
+#define vcpu_restore(x) do {} while(0)
+#define vcpu_switch(x) do {} while(0)
 static inline void VGICMaintenance(void) {}
 
 #endif /* end of !CONFIG_ARM_HYPERVISOR_SUPPORT */
diff --git a/libsel4/tools/syscall_stub_gen.py b/libsel4/tools/syscall_stub_gen.py
index 72aa21de7..cc8fd66e2 100644
--- a/libsel4/tools/syscall_stub_gen.py
+++ b/libsel4/tools/syscall_stub_gen.py
@@ -241,6 +241,9 @@ def init_arch_types(wordsize):
             CapType("seL4_ARM_PageDirectory", wordsize),
             CapType("seL4_ARM_ASIDControl", wordsize),
             CapType("seL4_ARM_ASIDPool", wordsize),
+            CapType("seL4_ARM_VCPU", wordsize),
+            CapType("seL4_ARM_IOSpace", wordsize),
+            CapType("seL4_ARM_IOPageTable", wordsize),
             StructType("seL4_UserContext", wordsize * 17, wordsize),
         ],
 
diff --git a/src/arch/arm/32/kernel/vspace.c b/src/arch/arm/32/kernel/vspace.c
index 50fa17164..b94d1006b 100644
--- a/src/arch/arm/32/kernel/vspace.c
+++ b/src/arch/arm/32/kernel/vspace.c
@@ -28,6 +28,7 @@
 #include <plat/machine/hardware.h>
 #include <armv/context_switch.h>
 #include <arch/object/iospace.h>
+#include <arch/object/vcpu.h>
 
 #ifdef CONFIG_BENCHMARK_TRACK_KERNEL_ENTRIES
 #include <benchmark_track.h>