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?

As an example of why I am asking, here is a build step that I have logged:

gcc --sysroot=/home/mb/seL4/build -I../kernel/include -I../kernel/include/64 -I../kernel/include/arch/riscv -I../kernel/include/arch/riscv/arch/64 -I../kernel/include/plat/spike -I../kernel/include/plat/spike/plat/64 -I../kernel/libsel4/include -I../kernel/libsel4/arch_include/riscv -I../kernel/libsel4/sel4_arch_include/riscv64 -I../kernel/libsel4/sel4_plat_include/spike -I../kernel/libsel4/mode_include/64 -Ikernel/gen_config -Ikernel/autoconf -Ikernel/gen_headers -march=rv64imac -mabi=lp64 -D__KERNEL_64__ -O2 -g -DNDEBUG -nostdinc -nostdlib -O2 -DHAVE_AUTOCONF -DDEBUG -g -ggdb -mcmodel=medany -fno-pic -fno-pie -fno-stack-protector -fno-asynchronous-unwind-tables -std=c99 -Wall -Werror -Wstrict-prototypes -Wmissing-prototypes -Wnested-externs -Wmissing-declarations -Wundef -Wpointer-arith -Wno-nonnull -ffreestanding -E -P -MD -MT kernel/CMakeFiles/kernel_bf_gen_target_1_pbf_temp_lib.dir/kernel_bf_gen_target_1_pbf_temp.c.obj -MF kernel/CMakeFiles/kernel_bf_gen_target_1_pbf_temp_lib.dir/kernel_bf_gen_target_1_pbf_temp.c.obj.d -o kernel/CMakeFiles/kernel_bf_gen_target_1_pbf_temp_lib.dir/kernel_bf_gen_target_1_pbf_temp.c.obj -c kernel/kernel_bf_gen_target_1_pbf_temp.c

This command line invokes gcc and at its end there is "-c kernel/kernel_bf_gen_target_1_pbf_temp.c", where the ".c"-file is a bitfields file. GCC should complain about the file format yet it does not. How is this achieved? I guess there must be something that presents the bitfields file in C syntax to GCC. How is this achieved?

Regards
Mike