Why is 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)
1 Like
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)