Here you can download a DSL compiler, used to define and manipulate bitfields (in C), in a structured way, with automatic generation of Isabelle/HOL correctness proofs.
This software was developed as part of the L4.verified project, where it was used to generate code to create and access tagged unions of packed bitfields, in a manner consistent with the C translation used in the project, together with automatically generated (and proved) correctness theorems. For further details, see the associated publication: Cock_08.
COPYRIGHT
file in the
distribution.
Installation instructions can be found in the README
file
contained in the distribution.