halt (kernel/src/arch/arm/64/idle.c) defined with the
__attribute__((noinline)) function attribute? I don’t see a problem with inlining this function.
The binary verification tool chain can’t handle the instructions for the
halt function, and relies on those instruction not appearing inside other functions. We prove that
halt is never called, so if it’s not inlined, the BV tool chain will never hit it.
halt is not performance critical, so there is no impact in not inlining it)
It might be worth adding a comment in the code explaining this. There are some places where the verification directs things, and this is not intuitively clear when looking at the code.
Are you interested to make a PR, @Jack.Chen ?
Sure, I’ll make a PR later. (would be my first contribution to the official seL4 repo)