Verification requires packed structures for reasoning (no implicit
padding).
The FPU context starts with 64-bit words, which the C parser assumes
have 8-byte alignment. Unfortunately, for this version of the kernel,
aarch32 has an odd number of word_t (32-bit) registers, resulting in an
extra word of implicit padding.
This type of manual padding is naturally fragile and will break as soon
as a user register is added or removed from the user context.
Signed-off-by: Rafal Kolanski <rafal.kolanski@data61.csiro.au>
f473021686