Hi,
This function, and many others, is generated by a tool called the 'bitfield generator' in tools/bitfield_gen.py It takes as input files ending in .bf, and can produce both C code and proofs said code. If you were to look in include/arch/arm/arch/object/structures.bf you would find a block structure called 'thread_state' with a field member called 'tcbQueued'. The bitfield generator takes this data structure description and generates all the relevant getter, setter and construction methods.
So during the build a file called 'arch/object/structures_gen.h' will get generated from this .bf file using the bitfield_gen.py tool in the Makefile rule '%_gen.h:' that contains all the functions. This file gets removed after compilation when doing standalone kernel builds.
Adrian
On 29/10/14 03:10, Yuxin Ren wrote:
Hi Kenneth,
After you build the kernel, you can find its definition in build/kernelkernel_final.c file.
But I do no know how it is generated.
I guess it is generated by some scripts or preprocessor.
I also hope the answer from sel4 expert.
Best,
Yuxin
On Tue, Oct 28, 2014 at 3:59 AM, chengkunck@gmail.commailto:chengkunck@gmail.com