That's not really relevant when talking about the linux kernel, though, is it ? There's tons and tons of open-source code that could just run clang-analyze today and eliminate swathes of memory bugs.
Static checker can work in principle on binary code. Alternatively, one can annotate API the library provides for the static checker. This is especially feasible with C where API types and usage is typically rather simple. Clearly, this implies trusting API to be implemented correctly or at least using the static checker to prove that memory-safety bugs are originated in the library, not in the application code.
