I'm all in C, too: kernel drivers from wifi chipset vendors. There's one C compiler we can use (gcc) and we're even restricted to working with a specific version (because cross compiling). We have to be very careful about changing any of the code because we have to integrate any changes into the next drop of the vendors' code. Static analysis is our best bet. Is a really interesting problem.