Elab bitfields: check size of type <=32bit rather than checking rank

[amosr]

Hello,

I had an issue with bitfields when using standard headers from newlib on ARM. The uint32_t typedef was defined as unsigned long, so the bitfield elaborator was complaining even though it was still only 32 bits. To fix this, I've changed the test in Elab.ml to check the size of the integer rather than the rank. I haven't gone through all the details of Bitfields.ml, but it looks like the logic depends on the size being <=32 rather than the rank, so I believe it is still correct.

I've added a test case but this is a bit tricky to run automatically, since it relies on a specific 32-bit configuration. I also manually inspected the generated assembly for ARM-v7m and it was correct.

Issue 315 sounds superficially similar, but this is a much simpler change as it still only supports 32-bit values. This change just allows you to refer to them with another name.

Thanks,
Amos

---

When desugaring a bitfield, allow any integral type that is 32 bits
or smaller. Previously this was checking the rank of the type rather
than the size.

This rank check caused issues with standard headers that
declare uint32_t to be an unsigned long rather than an
unsigned int. Here, any bitfields declared as uint32_t were
failing to compile even though they are still actually 32 bits.

[xavierleroy]

Thank you for the suggestion and the code. I agree that CompCert should support more types for bitfields than allowed by the C standards, eventually. Right now I'm busy with teaching, but I'll come back to this issue and to your proposal in a few weeks.

[xavierleroy]

Thank you for your patience and for this contribution. I like the proposed change: it makes bitfields more usable, while remaining within the limitations of CompCert's current bitfield packing schema. Merging now!