update CAVEATS text to include security proofs
bf gen: Fix: Prevent using stdout when writing HOL defs/proofs.

Stdout is not suitable as an output target for these things.
bf gen: Fix: Check UMM types is known before generating HOL proofs.
bf gen: Add a backend for AutoCorres.

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.
Ignore generated libsel4 headers.
libsel4: Turn seL4_MsgMaxLength into an enum.

This has no effect on the code, but makes this value visible as a named
constant in Isabelle when importing C sources. It avoids us having to reference
120 as a magic number in numerous proofs.
Merge branch master into experimental
trivial: fix string typo.