Hi!

I am new to this list so please forgive me if this question has been asked before.

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.

An example of that would be file

kernel/libsel4/mode_include/64/sel4/shared_types.bf

which can be obtained (as part of an entire source tree, of course) via repo init -u https://github.com/seL4/sel4test-manifest.git followed by repo sync.

What I find curious is that these files do not adhere to (common) C syntax yet they are fed into GCC and GCC swallows them.

This file format appears to be an extension to GCC. I could not find any documentation on any such extension. I would be grateful if anyone could point me to some kind of documentation pertaining to it.

Regards

Mike