This commit adds a two new output targets for the bitfield generator,
--autocorres-defs and --autocorres-proofs. These produce, respectively,
abstract definitions of the generated C functions suitable for use in
AutoCorres proofs and WP/simp lemmas suitable for use within AutoCorres proofs
of functions that call the generated C functions. Existing behaviour and
functionality should be unaffected.
5ee3971563