Thanks a lot for answering.

I have to ask a follow-up question. How does the bitfields tool chime in with the rest of the build process?

Here is a build step that I have logged: 

Den mån 13 maj 2019 kl 15:34 skrev G. Branden Robinson <g.branden.robinson@gmail.com>:
Hi, Mike!

At 2019-05-13T14:21:41+0200, Mike Epoch wrote:
> I am new to this list so please forgive me if this question has been
> asked before.

No worries; it's a low-traffic list.

> The seL4 code base contains a slew of files with a file type of "bf".
> These files seem to define packed structs that are to fit into words
> or d-words.

Yes.  They're called "bitfields", and you can read more about them here:

https://ts.data61.csiro.au/publications/nictaabstracts/Cock_08.abstract.pml

Regards,
Branden