vcpu: add padding to keep vcpu struct packed

Add padding to keep vcpu struct packed on 32-bit platforms. This doesn't
change the size on 32-bit platforms, because the compiler would insert
padding itself. It does increase the size of the struct by one word
on 64-bit platforms, but it remains below 2^vcpuBits.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

include/arch/arm/arch/object/vcpu.h

@@ -78,11 +78,13 @@ struct vcpu {
     word_t regs[seL4_VCPUReg_Num];
     bool_t vppi_masked[n_VPPIEventIRQ];
 #ifdef CONFIG_VTIMER_UPDATE_VOFFSET
-    /* vTimer is 8-bytes wide and has same alignment requirement.
-     * The struct will remain packed on 32-bit platforms when n_VPPIEventIRQ
-     * is odd, but were it to become even, an extra word of padding will be
-     * necessary.
-     * */
+    word_t vcpu_padding;
+    /* vTimer is 8-bytes wide and has the same 8-byte alignment requirement.
+     * If the sum of n_VPPIEventIRQ and seL4_VCPUReg_Num is even, we do not need
+     * extra padding. If the sum is odd we do. It currently is odd, so the extra
+     * padding above is necessary for the struct to remain packed on 32 bit
+     * platforms.
+     */
     struct vTimer virtTimer;
 #endif
 };