Alrighty, I believe I get it now. GCC preprocessing is used to generate
bitfield files. Then there is a Python utility that translates them to C
code at appropriate points during the build process.

Den mån 13 maj 2019 kl 16:51 skrev Mike Epoch <[email protected]
>:

> 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
>
> Den mån 13 maj 2019 kl 16:42 skrev Mike Epoch <
> [email protected]>:
>
>> 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 <
>> [email protected]>:
>>
>>> 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
>>>
>>
_______________________________________________
Devel mailing list
[email protected]
https://sel4.systems/lists/listinfo/devel

Reply via email to