forked from Imagelibrary/seL4
It has become clear that the 'packed' GCC attribute affects the memory semantics of C in a way that the verification tools do not understand. The bootinfo types are used by kernel boot code (not currently verified, but covered by binary verification) and should not use this attribute. This is a source-compatible but not binary-compatible change.