Minor fixes for other ARM platforms

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 */

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),
         ],
 

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>