c9f3c64162
Eliminate #ifdefs for BF_CANONICAL_RANGE in bitfield specifications, using the new field_ptr command. Use word_size expressions for some of the padding fields to make clearer where the sizes come from. The transformations in this commit are written to produce exactly identical output for code and proofs. In some rare cases, padding could in the future be rearranged to make more use of field_ptr, but these edits would create code differences and are left for later. It may now also be to share more blocks between generic 32 and 64 definitions if they only reference word_size. This is also left for later to reduce noise. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems> |
||
|---|---|---|
| .. | ||
| arm | ||
| riscv/arch | ||
| x86/arch | ||