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