To some extent, yes: it leaves it up to the decisions of the compiler as to when it wants to inline functions, so depending on your optimisation settings the compile might still choose to inline functions. And, since they are now all publicly visible, without linker garbage collection function definitions for the libsel4 functions which you don't use will also be emitted.
So, maybe. `static inline` and the default/public options are hints to the compiler that it might choose not to obey, depending on your optimisation settings. Julia ________________________________________ From: Yanfeng Liu via Devel <[email protected]> Sent: Tuesday, 2 June 2026 10:58 To: [email protected] Subject: [seL4] Re: libsel4 status Julia, Thanks a lot for teaching the LibSel4FunctionAttributes choice. Can I confirm that setting it to "public" or "default" will reduce usage of inline and the size of programs? I will try them later if above understanding is correct. Regards, yf On Sun, 2026-05-31 at 23:45 +0000, Julia Vassiliki via Devel wrote: > Hi yf, > > libsel4 code packaged as part of the seL4 repo is for production, > yes. It is used by all downstream projects that I know of. > > You can configure inline-ness of the libsel4 functions using the > `LibSel4FunctionAttributes` cmake configure option: > > https://github.com/seL4/seL4/blob/15.0.0/libsel4/CMakeLists.txt > > In our use, we haven't seen excessive code bloat from inline > functions, however, and generally I'd expect for these sorts of small > functions it would not make much of a difference. When inclined on > Aarch64, my experience is that an seL4_Signal will only take a few > instructions. > > Are you running into code bloat issues from the inline functions > (i.e. is there some case where this isn't true?), or is this > hypothetical/preference? > > Julia > > > ________________________________ > From: Yanfeng Liu via Devel <[email protected]> > Sent: Saturday, May 30, 2026 1:56:57 PM > To: [email protected] <[email protected]> > Subject: [seL4] libsel4 status > > Dear experts, > > It seems that currently libsel4 has many inlined functions thus user > space code size is large. > > I am wondering if this is really necessary? > > If current libsel4 is not for production use, then it doesnt matter. > Otherwise I am wondering if we need support size optimized config as > well? I am hoping that libsel4 changes wont affect kernel > verification? > > Regards, > yf > > > > > _______________________________________________ > Devel mailing list -- [email protected] > To unsubscribe send an email to [email protected] > > > This email and any files transmitted with it may contain confidential > information. If you believe you have received this email or any of > its contents in error, please notify me immediately by return email > and destroy this email. Do not use, disseminate, forward, print or > copy any contents of an email received in error. > > _______________________________________________ > Devel mailing list -- [email protected] > To unsubscribe send an email to [email protected] _______________________________________________ Devel mailing list -- [email protected] To unsubscribe send an email to [email protected] This email and any files transmitted with it may contain confidential information. If you believe you have received this email or any of its contents in error, please notify me immediately by return email and destroy this email. Do not use, disseminate, forward, print or copy any contents of an email received in error. _______________________________________________ Devel mailing list -- [email protected] To unsubscribe send an email to [email protected]
