We have the notable advantage that the kernel is written in a stereotyped
subset of C (as is true of any program that's not written by a frothing
madman). So the tools can use that, and (as sparse and GCC do) can rely on
user annotations, as well as erring on the side of paranoia.