Add the new block command
field_ptr(align) name size
as an abbreviation for
padding size - canonical + align
field_high name canonical - align
The (align) part is optional. If left out, align is 0.
This is useful for removing #ifdefs for pointer storage that are trying
to achieve constant size over different canonical bit representations.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Allow arithmetic integer expressions in all places where previously
only integer literals were allowed.
The operators +, -, *, / and % are supported. Additionally, in field,
field_high, and padding specifications, the constants "word_size" and
"canonical" are available.
This enables more readable bitfield specifications without changing
any of the code and proof generation. Produces identical output to
before.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Remove manual table of contents for rendering on the docsite, which will
provide an automatic TOC.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Add a user manual for the bitfield generator that documents syntax,
semantics and basic concepts. Should also be able to serve as main
spec for what the tool is supposed to do.
Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
