[rapidlua]

> How to manage pointer+offset address integrity/legality inside the kernel (for instance) has a proof by examples a-plenty in the other code

Let me provide some context here. These annotations aren’t there to help the compiler/linter. They exist to aid external tooling. Kernel can load BPF programs (JIT-compiled bytecode). BPF can invoke kernel functions and also some kernel entities can be implemented or augmented with BPF.

It is paramount to ensure that types are compatible at the boundaries and that constraints such as RCU locking are respected.

Kernel build records type info in a BTF blob. Some aspects aren’t captured in the type system, such as rcu facet, this is what the annotations are used for. The verifier relies on the BTF.